AI evidence extraction

Advancing Mathematics Research with AI-Driven Formal Proof Search

George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi et al. · arXiv (Cornell University) · 2026

AI-generated evidence extraction, verified across multiple analytical personas. Not a substitute for the peer-reviewed original.

9/10

Relevance

2/2

Quality (LMQS)

Evidence

Citations

0.00

FWCI

Methodology & findings

Study design

Systematic evaluation of AI-driven formal proof search agents (four agent variants: basic, basic with AlphaProof, evolutionary, and full-featured) applied to three problem sets: 353 Erdős problems from the Formal Conjectures repository, 492 OEIS conjectures, and application to open research problems in optimization, graph theory, algebraic geometry, additive combinatorics, and quantum optics.

Main result

The full-featured 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. "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."

Research paradigm

Computational mathematics with empirical validation on open research problems

Author conclusions

"Our results demonstrate the utility of LLM-powered formal proof search as a tool for mathematics research, and point to an ongoing shift from specialized trained systems toward simple agentic loops as LLMs become more capable." The authors further conclude: "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. Our results support this vision. Our mathematician collaborators found that proof attempts by our agents enhanced their understanding of a problem, even when an agent could not prove the claim at hand."

Risk of bias

Selection bias in problem choice: only formalized problems in repositories were evaluated; Stochastic variance in agent performance; Model bias inherited from underlying LLMs (Gemini 3.1 Pro, Gemini 3.0 Flash); Confirmation bias: problems solved may be inherently more tractable to formal methods; Selection bias: Only 9 out of 353 Erdős problems were solvable; the agent's success is concentrated in specific mathematical domains where Lean libraries are mature; Measurement bias: High variance in per-problem inference costs due to stochastic nature of agents; variance not fully quantified; Model bias: Agents inherit biases of underlying LLMs (Gemini 3.1 Pro, Gemini 3.0 Flash); Hallucination bias: Documented instances where agents claimed lemmas were established results when they were actually hallucinations; Formalization bias: Dependency on correct Lean formalization; misformalizations detected post-hoc (e.g., Erdős #125, #741); Computational resource bias: Cost-based comparisons favor agents with access to more computational budget; Selection bias: choice to run on Erdős problems where Lean formalizations existed; Problem tractability bias: success concentrated in combinatorics, convex optimization, and number theory with mature Lean libraries; LLM inherent biases inherited by the agents; High variance in search outcomes across stochastic agent executions

Limitations

"At present, our agents' successes are concentrated in areas such as combinatorics, convex optimization, and number theory, where Lean's mathematics library is mature and tasks often decompose into tractable subgoals
Even most Erdős problems remain out of reach, let alone problems that require extensive new theory
Additionally, our agents inherit the biases of their underlying LLMs and exhibit high search variance." The failure analysis revealed that agents "frequently offloaded a problem's core difficulty into a single sorry within a helper lemma that reiterated the target statement in a slightly different form" and "for several problems, the top sketches relied on lemmas marked with sorry that the agent claimed were established results in the mathematical literature
Upon manual inspection, these lemmas proved to be hallucinations."

Open questions raised

Expanding agent success beyond areas with mature Lean libraries (combinatorics, convex optimization, number theory)
Extending to problems requiring extensive new theory development
Characterizing and expanding the boundaries of agent capabilities
Reducing search variance and improving reproducibility
Closing the loop between AI-based conjecturing and proof systems
The authors identify that "[c]haracterizing the agents' boundaries and expanding them is an important direction for future work." They note that even most Erdős problems remain out of reach and that problems requiring extensive new theory are beyond current capabilities. The paper suggests future work in closing the loop between AI-based conjecturing (via Graffiti system) and AI-based proof, and in expanding the applicability of formal proof search beyond domains with mature Lean libraries.

Data: Formal Conjectures repository (Erdős problems): https://github.com/google-deepmind/formal-conjectures; OEIS (Online Encyclopedia of Integer Sequences) open conjectures: https://www.oeis.org/; All Lean proofs and select natural-language proofs: https://www.github.com/google-deepmind/alphaproof-nexus-results; OEIS (Online Encyclopedia of Integer Sequences): mentioned but not directly hosted by authors; AlphaProof Nexus results (all proofs): https://www.github.com/google-deepmind/alphaproof-nexus-results; Formal Conjectures repository (https://github.com/google-deepmind/formal-conjectures) containing 353 Erdős problem formalizations; Online Encyclopedia of Integer Sequences (OEIS) - 492 open conjectures autoformalized; Lean proofs and select natural-language proofs available at https://www.github.com/google-deepmind/alphaproof-nexus-resultsCode: https://www.github.com/google-deepmind/alphaproof-nexus-results; https://github.com/google-deepmind/formal-conjectures; https://www.github.com/google-deepmind/alphaproof-nexus-results (All Lean proofs and select natural-language proofs available); Formal Conjectures repository: https://github.com/google-deepmind/formal-conjectures; https://www.github.com/google-deepmind/alphaproof-nexus-results (AlphaProof Nexus results including all Lean proofs); https://www.erdosproblems.com (Erdős problems catalog); https://github.com/GasStationManager/SafeVerify (SafeVerify validation tool)Extracted from: pdfAgreement 46%

Explore related topics

Productivity Effects Research Productivity Empirical Study