# Advancing Mathematics Research with AI-Driven Formal Proof Search

arXiv: https://arxiv.org/abs/2605.22763 · HTML: https://mlsanity.com/paper/2605.22763/

## Key facts

- Cited by 23 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 19 of its 70 references that are in the map.
- First posted on arXiv 21 May 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 19 of 19)

- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Mathematical exploration and discovery at scale](https://mlsanity.com/paper/2511.02864/) (2025)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience](https://mlsanity.com/paper/2512.17260/) (2025)
- [Accelerating Scientific Research with Gemini: Case Studies and Common Techniques](https://mlsanity.com/paper/2602.03837/) (2026)
- [ODE Analysis of Stochastic Gradient Methods with Optimism and Anchoring for Minimax Problems](https://mlsanity.com/paper/1905.10899/) (2019)
- [Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4](https://mlsanity.com/paper/2410.16429/) (2024)
- [Point Convergence of Nesterov's Accelerated Gradient Method: An AI-Assisted Proof](https://mlsanity.com/paper/2510.23513/) (2025)
- [Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics](https://mlsanity.com/paper/2605.13171/) (2026)
- [Reinforced Generation of Combinatorial Structures: Hardness of Approximation](https://mlsanity.com/paper/2509.18057/) (2025)
- [Aletheia tackles FirstProof autonomously](https://mlsanity.com/paper/2602.21201/) (2026)
- [Reinforced Generation of Combinatorial Structures: Ramsey Numbers](https://mlsanity.com/paper/2603.09172/) (2026)
- [Progress in Formalizing Sphere Packing in Dimension 8](https://mlsanity.com/paper/2604.23468/) (2026)
- [An Improved Last-Iterate Convergence Rate for Anchored Gradient Descent Ascent](https://mlsanity.com/paper/2604.03782/) (2026)
- [Last-Iterate Convergence of Anchored Gradient Descent](https://mlsanity.com/paper/2604.12235/) (2026)

## Built on by (most cited first, 23 of 23)

- [LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks](https://mlsanity.com/paper/2606.03303/) (2026)
- [LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization](https://mlsanity.com/paper/2606.05400/) (2026)
- [Agentic Publication Protocol: An Attempt to Modernize Scientific Publication](https://mlsanity.com/paper/2606.27386/) (2026)
- [AI-Assisted Discovery of Convex Relaxations via Dual Agents](https://mlsanity.com/paper/2606.31182/) (2026)
- [A Formalization of the Mean-Field Derivation of the Vlasov Equation](https://mlsanity.com/paper/2607.08986/) (2026)
- [OEIS Open: How many conjectures can language models turn into theorems?](https://mlsanity.com/paper/2608.11941/) (2026)
- [The Problem Is the Problem: Towards Scalable Mathematical Discovery](https://mlsanity.com/paper/2608.16977/) (2026)
- [Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification](https://mlsanity.com/paper/2609.11319/) (2026)
- [Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science](https://mlsanity.com/paper/2609.15983/) (2026)
- [Can AI Refute Economic Theory? Evidence from Beyond the Knowledge Cutoff](https://mlsanity.com/paper/2606.05383/) (2026)
- [Stable Menus of Public Goods: AI-Enabled Progress](https://mlsanity.com/paper/2606.16989/) (2026)
- [Code evolution for link prediction in complex networks](https://mlsanity.com/paper/2606.26132/) (2026)
- [Theoria: Rewrite-Acceptability Verification over Informal Reasoning States](https://mlsanity.com/paper/2607.01223/) (2026)
- [Theoretical Foundations of max@k Reinforcement Learning](https://mlsanity.com/paper/2607.17823/) (2026)
- [Xeno-Interpretability: Investigating the Alien Minds of LLMs](https://mlsanity.com/paper/2609.20408/) (2026)
- [FrontierMath ErdHos](https://mlsanity.com/paper/2609.25050/) (2026)
- [When Does Structured Knowledge Help Neural Theorem Proving?](https://mlsanity.com/paper/2609.34460/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)
- [GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research](https://mlsanity.com/paper/2609.36663/) (2026)
- [Distribution Matching Evolutionary Algorithms for Rare Event Sampling](https://mlsanity.com/paper/2610.03833/) (2026)
- [LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs](https://mlsanity.com/paper/2610.11862/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)
- [Do Theorem Provers Need Theorem-Proving Agents? mini-Lean-agent: A Coding-Agent Baseline for Lean](https://mlsanity.com/paper/2610.17331/) (2026)

## Abstract (arXiv)

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 ErdHos 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 ErdHos 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.