Publications

We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework, GeoFormalizer represents informal problems in GeoIR, deterministically translates them into Lean 4, and iteratively repairs candidate statements using structural diagnostics and semantic evaluation. GeoProver constructs geometric proof plans, derives intermediate lemmas, and selectively algebraizes suitable subgoals through a library verified in Lean. Singular or SymPy may generate algebraic certificates, but all resulting proofs and counterexamples are checked by Lean’s kernel. Experiments across seven LLM backbones show substantial improvements in autoformalization, particularly for models with weaker direct translation performance. On 43 historical IMO geometry problems, GeoFormalizer generates formal statements that GeoProver proves in 29 cases; for the remaining 14, it constructs counterexamples verified in Lean and proves all repaired statements after expert correction. Together with IMO 2026 Problem 2, this yields, to the best of our knowledge, the largest reported collection of automated, kernel-checked Lean proofs for IMO geometry problems. On the 14 geometry statements in LEAP’s Lean-IMO-Bench, MechGeo proves 12 for the first time, formally refutes the remaining two, and proves both repaired statements. These results establish counterexample guided diagnosis, geometric reasoning, and certified symbolic computation as a practical foundation for trustworthy formal geometry.

AI reasoning has become a central focus in contemporary artificial intelligence, largely driven by the success of large language models. However, mathematical research, which is characterized by non-linear derivation paths, rigorous logical requirements, and protracted exploration cycles, poses severe challenges for existing reasoning systems. To overcome these limitations, we present the MechMath Agent Team (MMAT), which is a large language model driven agent designed to serve as a co-pilot throughout the full cycle of mathematical research. We design a tripartite Harness Architecture that decouples system responsibilities into Control, Execution, and Augmentation planes, thereby reconciling rigorous logical control with the agility demanded by open-ended research. Building upon this framework, we instantiate three specialized agents: a Knowledge Base Manager, a Natural Language Prover, and a Formal Language Prover, all operating in a closed loop to produce formally certified mathematical proofs. We evaluate MMAT on open problems in Number Theory, Algebraic Complexity Theory, Differential Algebra, Operator Algebra, and Inequalities. Across a two-month deployment, 11 problems have been solved, demonstrating its capacity to act as a co-pilot throughout the entire research cycle. The contributions are threefold: a general decoupled Harness Architecture for multi-agent mathematical reasoning, its concrete instantiation in the MMAT system, and empirical validation on a diverse suite of open problems.

We study the problem of deterministically computing the exact root of a sparse polynomial in the multivariate setting. Let $f \in \mathbb{F}[x_1,\ldots,x_n]$ be a nonzero polynomial that is an exact $e$-th power, say $f = g^e$. Suppose $f$ is $s$-sparse, has an individual degree of at most $d$, and a total degree of $D = \mathrm{tdeg}(f)$. We prove a sparsity bound on the base polynomial $g$: $|g|_0 \le s^{D(2d+2)/e + 1}.$ Based on this bound, we develop a deterministic algorithm that computes the base $g$. In contrast to the general deterministic factorization algorithm of Bhargava, Saraf, and Volkovich \cite{BhargavaSarafVolkovich2020}, which achieves only a quasi-polynomial dependence on the input parameters, our algorithm is \emph{polynomial-time} in the setting where the total degree $D$ is bounded. Specifically, the overall complexity is $\mathrm{poly}\left(s^{O(Dd)}, n, d, D\right) + s\cdot R(e),$ where $R(e)$ denotes the cost of constructing a single $e$-th root of a scalar in the base field $\mathbb{F}$, and, when $\operatorname{char}(\mathbb{F})\mid e$, the cost of computing a single Frobenius root of a scalar. This term is field-dependent, and over finite fields, $\mathbb{Q}$, or number fields with a suitable representation, it is absorbed into the polynomial complexity bound. Within the bounded total-degree regime, this yields a deterministic polynomial-time algorithm for exact-root computation.

In this paper, we establish degree obstructions to the equivalence of generalized Airy operators of the same type. As an application, we answer a question posed by Nicholas M. Katz in Inventiones Mathematicae (87, pp. 13-61,1987). The main results of Sections 3 and 4 were obtained through a close interactive collaboration between the authors and the artificial intelligence agent system MechMath Agent Team (MMAT).

In this note, we study the complexity of multiplication in skew polynomial rings over finite fields. We prove that the product of two elements in $\mathbb{F}_{q^n}[x;\sigma]$ of degree at most $d < n$ can be computed using $\widetilde O(d^{\omega_K-1}n)$ arithmetic operations over $\mathbb{F}_q$, where $\sigma$ is the $q$-Frobenius automorphism. This matches the conjectural upper bound of Caruso–Le Borgne and is quasi-optimal in view of the lower bound of Chen–Ye. The proof reduces the finite-field case to the split algebra case using the equivariant multiplication theory of Couveignes–Ezome, and then applies existing fast algorithms.

Recent advances in large language models (LLMs) and LLM-based agents have substantially improved the capabilities of automated theorem proving. However, for problems that require complex mathematical reasoning, current systems rarely succeed on the first try and must repeatedly modify their proof strategies. Existing approaches for handling failed attempts typically either iteratively fix errors within the proof or discard the entire proof and regenerate it from scratch. The former leads to progressively longer contexts, which progressively degrade the model’s ability to attend to the remaining unresolved subproblems, while the latter is inefficient, as it may abandon mostly correct reasoning due to localized errors. To address this dilemma, we propose MechMath, a novel agent system that employs a sorrifier-driven formal decomposition strategy. By leveraging the sorry placeholder in Lean to precisely isolate unresolved subgoals while preserving the surrounding verified proof structure, MechMath extracts each failed subproblem into a clean, self-contained context and resolves it independently. This avoids both the waste of full regeneration and the excessive context length induced by repeated repairs. Experimental results on challenging mathematical competition benchmarks, including IMO 2025, Putnam 2025, miniF2F, and a subset of ProverBench, demonstrate that our agent achieves significant advantages in proving efficiency.

In this paper, it is proved that any nonnegative integer can be written in the following form $\frac{x(x+1)}2+\frac{y(3y+1)}2+\frac{z(5z+1)}2,\,x,y,z\in\mathbb{N}.$ This settles the conjecture recorded as OEIS A287616. All parts of the proof have been formalized in Lean~4, with the exception of two results: one externally cited theorem and one statement verified by symbolic computation. Both the natural-language proof and the Lean formalization were generated by the MechMath Agent Team developed by the authors.

The binomial greatest common divisor (gcd) criterion recorded as OEIS A080170 is proven. The criterion also appears as conjecture (17) in Ralf Stephan’s list of OEIS conjectures. For $k\geq 2$, put $D(k)=\gcd_{2\leq q\leq k+1}\binom{qk}{k},\,n=k+1.$ If $P$ is the largest prime-power component $p^a$ exactly dividing $n$, then the criterion asserts $D(k)=1\,\Longleftrightarrow\,\frac{n}{P}>P.$ The proof is formalized in Lean and the Lean artifact is accepted as part of the Formal Conjectures project. Both the natural-language proof and the Lean formalization are generated by the MechMath Agent Team, an AI agent developed by the authors.

In this paper, we prove that output-sensitive sparse polynomial GCD computation over finite fields is NP-hard under BPP many-one reduction. More precisely, for two sparse univariate polynomials $f,g$ with finite field coefficients, there exists no randomized algorithm to compute $\mathrm{gcd}(f,g)$, which is polynomial-time in the sizes of $f,g,\mathrm{gcd}(f,g)$ under the standard complexity assumption NP$\nsubseteq$BPP. This settles the open problem posed as Challenge 5 in the book The Sparsity Challenges in the finite field setting. Furthermore, we show that the Roots of Unity Detection problem over finite fields is NP-hard; that is, determining whether the GCD of a sparse univariate polynomial and $x^n−1$ has nonzero degree is NP-hard.

In this paper, we show that deciding whether a sparse polynomial does not divide another sparse polynomial exactly over finite fields is NP-hard under BPP many-one reductions. Equivalently, the sparse polynomial divisibility test over finite fields is CoNP-hard. This resolves the long-standing open problem concerning the computational complexity of the divisibility test for sparse polynomials in the setting of finite fields.

Sparse polynomial multiplication is a fundamental problem in computer algebra and the theory of computation, and the development of a quasi-linear time output-sensitive multiplication algorithm has been posed as an open challenge. In this paper, a counterexample is provided to a previously claimed solution to this open problem for integer coefficients. By employing the existing quasi-linear modular-black-box interpolation algorithm, we are able to provide an algorithm with quasi-linear bit complexity for the integer coefficients setting. Furthermore, in the case of coefficients over a finite field, we obtain an algorithm whose bit complexity is linear in the number of terms, the logarithm of the degree, and the logarithm of the size of the finite field.

We prove the positive-real $n=9$ case of the Vasc cyclic inequality. The proof was obtained with human-guided assistance from the AI agent MechMath Agent Team: the human-readable part reduces the rational inequality to a homogeneous polynomial inequality, fixes a cyclic maximum, and parametrizes each sorted fixed-maximum cone by cumulative gaps; the finite part is a certificate covering all $8!=40320$ sorted cones. MechMath Agent Team generated the certificate verification workflow through Python tool calls, including the case split, verification programs, and terminal classifications. The published certificate has $36815$ coefficient leaves, $2236$ ordinary Polya multiplier leaves, and $1269$ AM-GM midpoint overlay leaves. Human authors audited the mathematical reductions and verification logic, and a separate artifact contains the certificate, an independent verifier, and a from-source rebuild route.

Applying Gröbner basis theory to concrete problems in Lean 4 remains difficult since the current formalization of multivariate polynomials is based on a non-computable representation and is therefore not suitable for efficient symbolic computation. As a result, computing Gröbner bases directly inside Lean is impractical for realistic examples. To address this issue, we propose a certificate-based approach that combines external computer algebra systems, such as SageMath or SymPy, with formal verification in Lean 4. Our approach uses a computable representation of multivariate polynomials in Lean to import and verify externally generated Gröbner basis computations. The external solver carries out the main algebraic computations, while the returned results are verified inside Lean. Based on this method, we develop automated tactics that transfer polynomial data between Lean and the external system and certify the returned results. These tactics support tasks such as remainder verification, Gröbner basis checking, ideal equality, and ideal or radical membership. This work provides a practical way to integrate external symbolic computation into Lean 4 while preserving the reliability of formal proof.