Source-linked AI summary
Advancing Mathematics Research with AI-Driven Formal Proof Search
George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferraiuolo, Henryk Michalewski, Edward Lockhart, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri
TL;DR
LLM reasoning is promising for mathematics but remains unreliable without verification, motivating formal proof search in Lean. This paper develops and evaluates AI agents that combine LLM generation with Lean validation on open research problems, reporting autonomous solutions across Erdős, OEIS, and several mathematical domains.
Problem
LLM-generated natural-language proofs can contain subtle logical errors requiring expensive expert review, while formal-proof search had not been broadly evaluated on open research-level problems.
Method
The paper develops AlphaProof Nexus agents that generate and refine Lean proof sketches, validate them with the Lean compiler, and optionally combine AlphaProof with evolutionary search.
Results
The full-featured agent solved 9 of 353 Erdős problems and proved 44/492 OEIS conjectures, with additional results across mathematics research.
Takeaways & Limitations
Formal proof search can support mathematics research by producing verified proof attempts and helping experts focus on unresolved subgoals and misformalizations.
Takeaways & Limitations
Successes are concentrated in areas with mature Lean libraries and tractable subgoals, while most Erdős problems and tasks requiring extensive new theory remain out of reach.
Abstract
from arXiv · showhide
Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method's ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.
1. Introduction
The paper addresses LLM unreliability in mathematics by generating formally verified Lean proofs and evaluates this approach on open research-level problems. Its agents solved problems across several mathematical domains, while a basic agent replicated the Erdős successes at higher cost on harder problems.
- LLM-generated natural-language proofs can contain subtle logical errors that require expensive expert review.
- Formal languages such as Lean mitigate these issues by automatically verifying every logical step.
- The framework includes a basic agent that independently searches for proofs with feedback from the Lean compiler and a full-featured agent using evolutionary coordination and AlphaProof.
- 9 of 353 Erdős problems were autonomously solved by the full-featured agent, including two questions open for 56 years, at a cost of a few hundred dollars per problem.
- 44/492 open OEIS conjectures were proved, alongside results in algebraic geometry, convex optimization, combinatorics, graph theory, and quantum optics research.
- The basic agent solved all 9 Erdős problems but incurred higher costs on harder problems, while the overall results demonstrate the utility of LLM-powered formal proof search for mathematics research.
2. AlphaProof Nexus
AlphaProof Nexus takes Lean theorem files with incomplete proofs and combines LLM-based sketch refinement, Lean validation, optional AlphaProof calls, and evolutionary search. Its agents preserve a sorry-free, compiler-checked proof as the successful output.
- Lean mechanically verifies definitions, theorems, and proofs by tracking pending goals after each tactic.
- The framework accepts a Lean theorem with sorry, its definitions and imports, and optional natural-language context or domain knowledge encoded in Lean.
- EVOLVE-BLOCK and EVOLVE-VALUE markers restrict where the agent may add proof material or change expressions, and successful runs output a sorry-free proof.
- Basic prover subagents independently refine sketches through multi-turn LLM episodes, using Lean compilation and error messages to direct subsequent turns.
- AlphaProof can fill missing sketch components with proofs, while disproofs and failures are returned to the prover as feedback.
- The evolutionary agent ranks shared sketches with Elo ratings based on plausibility, clarity, and novelty, then samples them using P-UCB-driven search; the full-featured agent combines this with AlphaProof.
3. Systematic Evaluation on Open Problems
The systematic evaluation applies the full-featured agent to formalized Erdős and OEIS problems and examines both successful constructions and failure modes. The results include substantial mathematical arguments, correction of misformalizations, and persistent failures involving unsupported helper lemmas.
- 353 formalized Erdős problems were attempted, with search terminated after 3000 episodes when no proof was found; 9/353 were solved and expert-validated.
- The agent constructed sophisticated Erdős solutions using infinite block unions, the Chinese Remainder Theorem, and sets avoiding length-3 arithmetic progressions.
- For Erdős #125, the agent resolved whether the lower density of a sumset is positive using an inductive thinning argument exploiting 3^m≈4^k.
- The agent exposed density misformalizations in Erdős #125 and #741(i), after which corrected lower- and upper-density statements were still resolved.
- Failed searches often hid the target difficulty behind sorry-marked helper lemmas or cited hallucinated literature results, underscoring the need for end-to-end formal verification.
- The agent proved 44 conjectures from 492 autoformalized OEIS questions after test lemmas checked initial sequence terms against their formal definitions.
4. Deployment in Mathematics Research
The agent was deployed across optimization, graph theory, algebraic geometry, and related research efforts, where it produced proofs, algorithmic improvements, and reformulations. These deployments combined formal proof search with problem-specific mathematical exploration.
- Optimization Theory: The agent proved an exact O(1/t) convergence rate for Anchored GDA by discovering a parameter schedule within an EVOLVE-VALUE block.
- Optimization Theory: The optimization proof used a discrete-time recurrence rather than the continuous-time ODE analysis used in previous work.
- Graph Theory: The agent proved a bipartite graph reconstruction algorithm under an additional type condition, while the unrestricted statement remains open.
- Graph Theory: The agent proved a graph-theory conjecture relating maximum spanning-tree leaves to independent sets in vertex neighborhoods.
- Algebraic Geometry: Agent (D) solved two of four open algebraic-geometry problems, including Zanello’s conjecture on log-concavity of pure O-sequences.
- Algebraic Geometry: Its algebraic-geometry argument used a reformulation of the Hilbert function and detailed case analysis of second-difference inequalities.
- Further Deployments: The agent also constructed intricate formal proofs for the Stacks Project and autonomously solved a real-valued variant of a problem from Green’s list, while the intended complex-valued case remained unresolved.
- Further Deployments: In quantum optics, the agent investigated monochromatic quantum-graph constructions corresponding to multipartite quantum states and resolved multiple conjectures of this form.
5. Impact of Agent Architecture and Model
The study compares agent architectures by solve rate, inference cost, and wall-clock time on Erdős problems. The full-featured agent helps most on the hardest problems but is less cost-efficient on many others.
- The evaluation compares four agents on six Erdős problems using solve rate against mean inference cost.The agents are basic, basic with AlphaProof, basic with evolution, and full-featured.
- For agents (A) and (B), increasing attempts traces a cost–performance Pareto frontier with diminishing marginal returns at higher budgets.The comparison groups K∈{1, 3, 6, 10} attempts, with error bars showing one standard error interval.
- The reported costs omit AlphaProof inference costs for agents (B) and (D), although adding an estimated $60 does not change the outcomes beyond the margin of error.
- Agents (A) and (B) perform similarly within the margin of error on four problems, while (B) is more efficient on problems 12(ii) and 125.
- Agent (D) offers 2x to 5x monetary savings on problems 138 and 125 but is roughly half as cost-efficient on the remaining problems.Its wall-clock advantage also concentrates on problems 138 and 125.
- The study also reports that Codex solved 7/9 problems, while Claude Code solved none.
6. Discussion
The discussion argues that formal proof search can support research-level mathematics while keeping proofs mechanically checkable. It also identifies concentrated successes, persistent failures, and a role for human–machine collaboration.
- Formal verification can filter AI-generated proofs so human experts focus review on arguments that warrant further attention.
- The basic agent matched the full-featured agent’s nine Erdős successes, while the full-featured agent retained an advantage on the hardest problems.The authors attribute the basic agent’s success to stronger LLMs and compiler feedback.
- Current successes concentrate in combinatorics, convex optimization, and number theory, where Lean’s library is mature and tasks often decompose into tractable subgoals.
- Most Erdős problems remain out of reach, especially problems requiring extensive new theory, and the agents exhibit bias from their underlying LLMs and high search variance.
- Collaborators report that formal proof sketches improved problem understanding, focused attention on unresolved subgoals, and exposed misformalizations.These observations support using formal proof search as a tool for both solving problems and deepening human understanding.
A. Materials and Methods
AlphaProof Nexus combines Lean-verified LLM proof generation with independent or evolutionary search. Its full-featured agent samples and rates proof sketches, uses targeted tools, and validates only uncompromised compiling candidates.
- Basic agent: The basic agent runs independent subagents from the same initial proof sketch, terminating the others when one finds a proof.
- Basic agent: Each basic-agent episode uses multi-turn LLM inference, search-and-replace edits, Lean compiler feedback, and final SafeVerify validation.
- Full-featured agent: The full-featured agent runs an asynchronous evolutionary loop that samples root and inspiration sketches, constructs prompts, and dispatches prover episodes.
- Population and validation: Only sketches that compile successfully and preserve the original theorem are added to the population database.
- Full-featured agent: Prover episodes can query AlphaProof and use structured edits, while validation retrieves cached subgoals or sends unresolved goals to AlphaProof before SafeVerify checks the completed proof.
- Population and rating: The rating model uses Plackett-Luce strengths with hierarchical Gamma priors and Gibbs sampling to estimate sketch quality.
- Population and rating: Rater agents compare P=7 sketches by strategy clarity, remaining-goal plausibility, and novelty, then update Elo ratings used for sampling.
- Evolutionary selection: P-UCB selects parent sketches from the top 64 Elo-ranked candidates, balancing exploitation with exploration through an empirically chosen c=0.2 bonus.
B.1. Related Work
Formal theorem proving has progressed from language-model-guided tactic search to systems that separate high-level planning from low-level elaboration. This work positions Lean as a medium for discovering new mathematics rather than only formalizing existing arguments.
- Formal Theorem Proving with LLMs: Formal theorem-proving systems use neural guidance for machine-checkable proof search, including tactic generation, premise selection, and external-prover interaction.Recent systems also separate proof planning from low-level elaboration, while AlphaProof demonstrated reinforcement-learning-based theorem proving at the Math Olympiad level.
- Formal Theorem Proving with LLMs: At the research level, AI-aided formal proofs have primarily verified results first derived in natural language.Examples include formalizations of AI-generated Erdős proofs and Viazovska’s sphere-packing proof.
- Formal Theorem Proving with LLMs: The paper uses Lean as a medium for novel mathematical discovery, extending prior work beyond formalizing natural-language arguments.Its evaluation targets open research-level problems rather than only competition mathematics or human-aided formalization.
- Evolution for Mathematical Discovery: Evolutionary search has been applied to mathematical program discovery, with FunSearch and AlphaEvolve providing precedents for LLM-guided construction and bound improvement.The full-featured agent reuses components of AlphaEvolve.
- Evaluation Context: The Erdős evaluation used all 353 Lean statements available in the Formal Conjectures repository, whose selection reflects community formalization choices and a bias toward Lean-amenable problems.The OEIS evaluation instead used 492 conjectures selected and formalized from an initial corpus of 2649 open conjectures.
B.3. Details on Comparisons across Agent Architectures and Models
The comparisons examine solve rate, cost, and wall-clock time across agent configurations, while also testing alternative models and AlphaProof as a standalone baseline. The results show stochastic costs, diminishing returns with larger attempt budgets, and failures for several alternative systems.
- Cost and Solve-Rate Comparisons: Cost distributions showed large variance across most problems and methods, highlighting the stochastic nature of the agent.Figure 9 reports computational costs for successful runs together with solve rates for each agent.
- Cost and Solve-Rate Comparisons: Solve rate and inference cost were compared across seven system configurations on nine Erdős problems.The configurations included basic, basic with AlphaProof, basic with evolution, full, and full variants with different asynchronous-agent counts.
- Wall-Clock Comparisons: Wall-clock distributions compared basic@K=10, basic with AlphaProof@K=10, and full under a 48-hour cutoff.Box plots encode medians, quartiles, whiskers, outliers, and single-success instances.
- Cost and Solve-Rate Comparisons: K=10 was identified as a strong default for the system.For basic and basic with AlphaProof, increasing K traces a cost–performance Pareto frontier with diminishing marginal returns at higher budgets.
- Model and Baseline Comparisons: None of the three additional basic-agent runs using Gemini 3.0 Flash, Gemini 3.1 Flash-Lite, or basic with AlphaProof solved an Erdős problem.Each run used K=100 and a 24-hour time budget.
- Model and Baseline Comparisons: AlphaProof alone solved none of the nine Erdős problems despite an approximate budget of 64 v6e TPU hours per problem.The baseline was run in tree-search inference mode.
B.4. Deformalized Lean Proofs
The deformalized proof constructs an infinite set from carefully spaced blocks whose modular structure prevents forbidden divisibility relations. A base-conversion function supplies the within-block progression-free property, while parameter bounds establish the required density.
- Construction Strategy: The proof constructs blocks that individually avoid the forbidden divisibility configuration and whose union is sufficiently dense.The construction controls block growth and modular residues to satisfy the lim inf condition.
- Within-Block Structure: The function f maps binary representations to ternary representations containing only 0s and 1s, so its image contains no 3-term arithmetic progressions.The relation f(a)+f(b)=2f(c) forces a=b=c.
- Modular Separation: Chinese-remainder parameters assign each block residues that distinguish elements in the same block from elements in later blocks.For each i, the construction chooses C_i satisfying C_i≡0 modulo F_i and C_i≡1 modulo M_i.
- Block Parameters: Each block is defined as B_i={P_i+V_i f(y) | y<X_i}, with Y_i controlling block width and spacing.The parameters P_i and X_i set the starting coordinate and capacity of each block.
- Avoiding Forbidden Relations: The cross-block case contradicts the required divisibility through incompatible residues modulo F_i.The relevant sum has residue 1 or 2 modulo F_i, whereas divisibility would require residue 0.
- Avoiding Forbidden Relations: The same-block case reduces divisibility to 2a=b+c, which becomes a forbidden three-term arithmetic progression in the image of f.Substitution and cancellation yield 2f(a′)=f(b′)+f(c′), contradicting the progression-free property.
- Density Bound: The density bound is established by considering whether N lies between consecutive blocks or inside a block.Both cases provide lower bounds for C(N)=|A∩{1,...,N}|.
Erdős #12-(ii)
The agent proves Erdős #12(ii): an infinite set avoids the stated divisibility configuration while retaining density at least N^(1−c) for every c>0 and sufficiently large N. The construction combines dense 3-AP-free sets, modularly separated blocks, and asymptotic growth comparisons.
- Construction: The construction uses pairwise coprime moduli, Chinese Remainder Theorem offsets, and Behrend-style dense 3-AP-free sets.The running products and CRT offsets separate blocks, while vectors on a sphere supply the 3-AP-free components.
- Construction: Base-(2m+1) encoding prevents carries, and the sphere restriction makes each block 3-AP-free and tightly clustered.Digits bounded by m ensure carry-free addition; the radius condition excludes 3-term arithmetic progressions.
- Verification: The global set A is formed from blocks A_k whose CRT conditions rule out cross-block divisibility configurations, while within-block cases reduce to forbidden 3-term progressions.Block separation is established by rapidly increasing dimensions and base exponents.
- Density: For c>0, the left asymptotic exponent has coefficient 1−c/2, exceeding the right coefficient 1−c, so the density inequality holds for sufficiently large k.The running product contributes only O(k^2), absorbed by the O(k^3) error terms.
- Context: The second question implies the first, but both proofs were retained because the agent found them independently after separate formalization.The paper reports that multiple proofs were initially found for the second question and one was selected for informalization.
Erdős #741-(i)
For Erdős #741(i), the agent resolves the corrected upper-density formulation affirmatively: every relevant set can be partitioned into two parts whose self-sumsets both have positive upper density. The proof alternates rapidly growing blocks and handles separately positive-density and zero-density cases.
- Result: The corrected question asks whether A can be partitioned as A=A_1⊔A_2 so that A_1+A_1 and A_2+A_2 both have positive upper density.The original wording was amended from natural density to upper density.
- Construction: An alternating block partition assigns consecutive intervals to A_1 and A_2, with block sizes growing fast enough that each new block dominates earlier elements.Odd-indexed intervals go to A_1 and even-indexed intervals to A_2.
- Case 1: If A has positive upper density, rapidly selected scales preserve density in each newly assigned block, giving both A_1 and A_2 positive upper density.Each component’s sumset then also has positive upper density.
- Case 2: If A has zero upper density but A+A has positive upper density, the proof applies a sumset bound at alternating scales to show each component self-sumset has positive upper density.The argument separates sums involving old elements from sums formed within the dominant new block.
- Case 2: The alternating-scale estimates give |(A_1+A_1)∩[1,N]|≥3cN/4 and |(A_2+A_2)∩[1,N]|≥3cN/4 along infinitely many scales.These bounds imply positive upper density for both self-sumsets.
- Formulation: The agent initially disproved a strict natural-density formulation, prompting correction to the upper-density interpretation before resolving the amended problem.The paper attributes the interpretation to an observation that Erdős likely intended positive upper density.
Erdős #26, More General Variant
The paper presents two further open-problem results. For Erdős #26, it constructs a divergent-reciprocal sequence whose shifted multiples always have upper density below 3/4; for Erdős #846, it constructs a planar set that cannot be finitely partitioned into no-three-collinear subsets.
- Erdős #26: There exists a sequence A with Σ_i1/A(i)=∞ such that for every k≥1, d(M(A+k))<1−ε for ε=1/4.The theorem gives the uniform bound d(M(A+k))<3/4 for all positive shifts.
- Erdős #26: The construction uses finite blocks, rapidly increasing indices, prime congruences, and the Chinese Remainder Theorem to control every shifted tail.For sufficiently late blocks, a prime q_k divides every shifted sequence element, confining the tail multiples to multiples of q_k.
- Erdős #26: The three-regime density estimate yields 0.1+0.2+1/29≈0.334<3/4 for the multiples of every shifted sequence.The cases cover the finite initial segment, a critical block, and the infinite tail.
- Erdős #846: For Erdős #846, the constructed infinite set A⊂ℝ² has at least n/2 points with no three collinear in every n-element subset, yet cannot be covered by finitely many such sets.This answers the stated finite-cover question negatively.
- Erdős #846: Each edge of an infinite complete graph maps to a planar point so that three points are collinear exactly when the corresponding edges form a triangle.Rapidly growing coordinates prevent accidental polynomial cancellations in the converse direction.
- Erdős #846: Every n-edge graph contains a bipartite subgraph with at least n/2 edges, yielding the no-three-collinear subset guarantee.If a finite cover existed, infinite Ramsey theory would produce a monochromatic triangle and therefore three collinear points in one color class.
- Additional result: The paper also records a Sidon-set bound: f(n)≥(n^2−100n−16)/16, so the minimum number of isolated sumset elements diverges.The estimate follows from standard Sidon sumset and difference-set bounds.
OEIS Conjectures
The paper proves OEIS conjectures by combining root-of-unity methods, coefficient bounds, asymptotic error control, and modular determinant arguments. It establishes the conjectured asymptotic expansion for integer-average subsets and an integer eighth-root generating-function result.
- Theorem A051293 concerns the number a_n of nonempty subsets of {1,…,n} whose elements have an integer average.
- A051293 asymptotics: The proof expresses a_n as a sum over subset sizes whose element sums are divisible by the subset cardinality, using roots-of-unity orthogonality.
- A051293 asymptotics: The root products are bounded by grouping terms into full periods and residual terms, yielding exponentially small remainder contributions.
- A051293 asymptotics: The proposed approximation f_n is compared with S_n through consecutive-difference errors, whose polynomial bounds establish the conjectured asymptotic expansion.
- A051293 asymptotics: The proof concludes that the accumulated remainder is negligible and explicitly establishes the conjectured asymptotic expansion.
- Hankel determinant generating function: For the Hankel determinant problem, congruences modulo 3 and 4 yield 3^n and 4^n divisibility, which combine to support an integer eighth root of A(x/3).
- Hankel determinant generating function: Writing A(x/3)=1+16Y(x), the proof constructs C(x)=1+2X(x) in Z⟦x⟧ with C(x)^8=A(x/3).
- The paper also states a weak bipartite graph reconstruction theorem for 2-connected graphs with pairwise distinct vertex types.
Log-Concavity of Hilbert Sequences
The paper proves Zanello’s conjecture that every pure O-sequence of codimension 3 and type 2 is log-concave. Its argument bounds second differences and analyzes cases arising from two maximal monomials.
- Background: Pure O-sequences are Hilbert functions of monomial Artinian level algebras and count monomials in pure finite order ideals.
- Motivation and result: Zanello’s conjecture identifies codimension 3 and type 2 as the remaining open case addressed by the theorem.
- Motivation and result: The main theorem states that every pure O-sequence of codimension 3 and type 2 is log-concave.
- Setup: The proof represents monomials by exponent vectors and uses finite order ideals, maximal monomials, socle degree, and type to decompose the sequence.
- Proof strategy: For two maximal monomials, the sequence is decomposed as H=f+g, and second-difference bounds give Δ²H(t)≤2.
- Proof strategy: Case analyses for lower and upper alternatives establish the inequalities needed for H(d−1)H(d+1)≤H(d)^2.
- Proof completion: Shift reduction and the remaining cases complete the log-concavity proof for all 0<d<e.
- Proof completion: The concluding argument applies the established inequalities across the full degree range and proves the theorem.