Visual Summary | Advancing Mathematics Research with AI-Driven Formal Proof Search

Summary (Overview)

First large-scale evaluation of AI-driven formal proof search on open research-level mathematics problems, using a framework called AlphaProof Nexus built on Lean and large language models (LLMs).
The full-featured agent autonomously resolved 9 of 353 open Erdős problems (at a cost of a few hundred dollars per problem), proved 44/492 OEIS conjectures, and contributed to open problems in optimization, graph theory, algebraic geometry, additive combinatorics, and quantum optics.
A basic agent (LLM generation + Lean verification loop) replicated the Erdős successes in post-hoc analysis, though at higher cost on the hardest problems, revealing that simple agentic loops are increasingly competitive as LLMs improve.
Key technical innovations include evolutionary search over proof sketches (with Elo-rated ranking), integration of AlphaProof (a reinforcement-learning-based theorem prover) as a tool, and EVOLVE-VALUE markers allowing the agent to search over both proofs and parameter values simultaneously.
The paper identifies failure modes (e.g., offloading difficulty into sorry placeholders, hallucinated lemmas) and argues for formal verification as a filter for AI-generated mathematics.

Introduction and Theoretical Foundation

Large language models (LLMs) have shown remarkable promise in solving complex mathematics problems, but their unreliability—particularly the risk of "hallucinations" in natural-language proofs—limits their utility in research. Subtle logical errors can cascade through a proof, and expert review is expensive.

Formal proof languages like Lean [43] mitigate this: a compiler automatically verifies every logical step, so a proof is correct if and only if it compiles without sorry tactics (which close goals unchecked). The paper's central thesis is that LLM-generated formal proofs can serve as a reliable, scalable tool for mathematics research.

The authors build on prior work in:

AlphaProof [29]: a reinforcement-learning system for olympiad-level Lean theorem proving.
AlphaEvolve [46]: an evolutionary algorithm for code generation.
Ralph loops [31]: iterative LLM inference loops with compiler feedback.

The key theoretical insight is that formal verification acts as a filter: it automatically rejects hallucinated arguments, allowing the agent to search a vast space of proof sketches without human oversight at every step.

Methodology

Lean as a Proof Environment

Lean [43] is a proof assistant where definitions, theorems, and proofs are mechanically verified code. A proof is constructed via tactics (elementary proof steps); the compiler tracks pending goals after each tactic. A proof is correct if it reaches a state with no pending goals and no sorry tactics.

AlphaProof Nexus Framework

The framework takes as input a proof sketch: a Lean file with the target theorem stated, a sorry in place of the proof, and optional natural-language context. The sketch is annotated with:

EVOLVE-BLOCK markers: regions where the agent may introduce helper lemmas, definitions, and proof steps.
EVOLVE-VALUE markers: expressions (e.g., parameters) whose values the agent may change.

Agent Architectures

Four agents were compared:

Agent	Description
(A) Basic	Independent prover subagents running "Ralph loops": multi-turn LLM inference (Gemini 3.1 Pro) with chain-of-thought, search-and-replace tool, and Lean compiler feedback after each turn.
(B) Basic + AlphaProof	Agent (A) extended with the ability to query AlphaProof to fill missing proof parts; proofs are substituted directly, while disproofs/failures are fed back into the prompt.
(C) Evolutionary	Prover subagents sample from and contribute to a shared population database of sketches. A pool of rating agents (Gemini 3.0 Flash) ranks sketches by plausibility, clarity, and novelty, aggregated into Elo ratings, with sampling driven by the P-UCB formula [30, 55].
(D) Full-featured	Combines (B) and (C): evolutionary search + AlphaProof tool use. Used for the large-scale exploration.

Evaluation Protocol

Erdős problems: 353 formalized statements from the Formal Conjectures repository [23]; search terminated after 3000 episodes per problem.
OEIS: 492 open questions autoformalized with Gemini, with "test lemmas" verifying the first few terms as a guard against misformalization.
Cost analysis: Reported in USD as a common currency; for agents (A)/(B), 100 independent attempts were grouped into chunks of size $K \in \{1, 3, 6, 10\}$ to simulate parallel subagent scenarios.

Empirical Validation / Results

Erdős Problems

The full-featured agent solved 9 of 353 problems. Key examples:

ID	Conjecture Summary	Proof Technique
12 (i)	(1970) Existence of $A \subset \mathbb{Z}^{+}$ s.t. $a \nmid (b+c)$ with $	A \cap [1, N]
12 (ii)	(1970) Existence of $A \subset \mathbb{Z}^{+}$ s.t. $a \nmid (b+c)$ with $	A \cap [1, N]
125	(1996) $\{ \sum \epsilon_k 3^k \} + \{ \sum \epsilon_j 4^j \}$ has lower density zero	Inductive thinning via Diophantine approx. $3^m \approx 4^k$
138*	(1981) Van der Waerden numbers satisfy $W(k+1) - W(k) \to \infty$	Greedy coloring extension with monochromatic intersection lemma
152	(1994) Sidon sets $A$ contain many isolated points in $A + A$	Elementary argument by bounds on interior points
741 (i)/(ii)	(1994) Decomposition of sets with positive upper density	Bounding of upper density via cases; explicit construction
846	(1992) Existence of infinite set with non-collinear subsets	Label $K_{\infty}$ vertices, apply map $\{i,j\} \mapsto (x_i + x_j, x_i^2 + x_i x_j + x_j^2)$
26*	(1995) Existence of $A$ with upper density of $A + k$ $< 1 - \frac{1}{4}$	Block-based construction using primes and CRT

The asterisk indicates a variant of the main problem; #26 is a more general variant not posed by Erdős himself.

OEIS Results

The agent proved 44/492 open OEIS conjectures, all verified as correctly formalized and previously unproven by manual review.

Other Domains

Optimization: Proved an exact $O(1/k)$ convergence rate for Anchored Gradient Descent-Ascent (GDA), tightening the bound of [52]. The agent discovered a novel parameter schedule via EVOLVE-VALUE markers.
Graph theory: Proved a variant of the graph reconstruction conjecture for bipartite graphs under an additional type condition; proved a conjecture from Grafiti [19] on spanning tree leaves.
Algebraic geometry: Solved Zanello's conjecture on log-concavity of pure O-sequences for codimension 3, type 2—surprising because log-concavity fails for many other families.
Additive combinatorics: Helped resolve problem #57 from Ben Green's list [27] by proving a counterexample to the complex-valued variant.
Quantum optics: Resolved multiple conjectures on monochromatic quantum graphs with $N = d$ for $d = 4, 6, 10$ .

Agent Comparison (Fig. 3)

Agents (A) and (B) perform similarly on 4/6 problems; (B) is more efficient on #12(ii) and #125.
Agent (D) outperforms (A)/(B) on #138 and #125 (2x–5x cost savings) but is ~2x less cost-efficient elsewhere.
Standalone AlphaProof, smaller models (Gemini 3.0 Flash, 3.1 Flash-Lite), and Claude Code solved zero problems.
Codex (GPT-5.5) solved 7/9 problems, failing #152 and #125 within 12 hours.
AlphaProof cost ~~27.5 TPU hours (~~$60 USD) per problem on v6e TPUs.

Failure Analysis

Two dominant failure modes:

sorry offloading: The agent placed the core difficulty into a helper lemma restating the target, which explicit prompting failed to prevent.
Hallucinated lemmas: Top sketches relied on lemmas marked sorry that the agent claimed were established results but were fabricated.

Theoretical and Practical Implications

Theoretical Significance

Demonstrates that LLM + formal verification can solve open research problems, not just competition exercises.
The basic agent's success is surprising: simple agentic loops with compiler feedback are now competitive with sophisticated evolutionary systems, suggesting a paradigm shift toward simpler architectures as LLMs improve.
The evolutionary framework bridges the gap between evolutionary algorithms (which assume a graduated fitness landscape) and formal proof evaluation (which is binary) via Elo-rated sketch ranking.

Practical Implications

Cost-effectiveness: A few hundred dollars per problem makes AI proof search accessible to individual researchers.
Misformalization detection: The agent identified ambiguities in the informal statements of Erdős problems #125 and #741(i) (e.g., "density" → "lower density").
Human-AI partnership: Proof attempts enhanced mathematicians' understanding even when unsuccessful; formal sketches let experts focus on unresolved subgoals rather than re-verifying entire arguments.
Limitations: Success is concentrated in areas with mature Lean libraries (combinatorics, number theory, convex optimization); problems requiring extensive new theory remain out of reach.

Conclusion

The paper provides the first large-scale demonstration of AI-driven formal proof search on open research-level mathematics. The full-featured agent (AlphaProof Nexus) solved 9 Erdős problems, 44 OEIS conjectures, and contributed to multiple active research areas. The post-hoc finding that a basic agent (LLM + Lean compiler feedback) replicates most successes suggests that the field is shifting toward simple agentic loops as LLM capabilities grow.

Future directions include:

Characterizing and expanding the boundaries of what these agents can solve.
Addressing failure modes (e.g., sorry offloading, hallucinated lemmas).
Closing the loop between AI-based conjecturing (e.g., Grafiti) and AI-based proof.
Extending to problems requiring new mathematical theory.

"We built AlphaProof Nexus with the belief that the future of mathematics lies in human-machine partnership, where interactive AI tools serve to expand a mathematician's creative capacity."

All Lean proofs and select natural-language proofs are publicly available at: https://www.github.com/google-deepmind/alphaproof-nexus-results.