mlsanityData to 14 Oct 2026

Advancing Mathematics Research with AI-Driven Formal Proof Search

arXiv 2605.22763 ↗First posted 21 May 2026cs.AIcited by 23

On the map: LLM reasoning → Mathematical reasoning

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.

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.

Builds on

19 of 70 references.

Closest ancestors · 3

Same direction, newest first

  1. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoning26 Sep
  2. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning15 Apr
  3. 2020Generative Language Modeling for Automated Theorem Proving7 Sep

Other references · 16

  1. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  2. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
  3. 2025Mathematical exploration and discovery at scalecited by 77
  4. 2025Aristotle: IMO-level Automated Theorem Provingcited by 58
  5. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 44
  6. 2026Accelerating Scientific Research with Gemini: Case Studies and Common Techniquescited by 29
  7. 2019ODE Analysis of Stochastic Gradient Methods with Optimism and Anchoring for Minimax Problemscited by 18
  8. 2024Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4cited by 18
  9. 2025Point Convergence of Nesterov's Accelerated Gradient Method: An AI-Assisted Proofcited by 11
  10. 2026Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematicscited by 10
  11. 2025Reinforced Generation of Combinatorial Structures: Hardness of Approximationcited by 9
  12. 2026Aletheia tackles FirstProof autonomouslycited by 9
4 more
  1. 2026Reinforced Generation of Combinatorial Structures: Ramsey Numberscited by 9
  2. 2026Progress in Formalizing Sphere Packing in Dimension 8cited by 9
  3. 2026An Improved Last-Iterate Convergence Rate for Anchored Gradient Descent Ascentcited by 3
  4. 2026Last-Iterate Convergence of Anchored Gradient Descentcited by 3

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 23.

23 papers.

Sort:

By area:

  1. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworkscited by 12
  2. 2026LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalizationcited by 12
  3. 2026Agentic Publication Protocol: An Attempt to Modernize Scientific Publicationcited by 2
  4. 2026AI-Assisted Discovery of Convex Relaxations via Dual Agentscited by 2
  5. 2026A Formalization of the Mean-Field Derivation of the Vlasov Equationcited by 2
  6. 2026OEIS Open: How many conjectures can language models turn into theorems?cited by 2
  7. 2026The Problem Is the Problem: Towards Scalable Mathematical Discoverycited by 2
  8. 2026Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verificationcited by 1
  9. 2026Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Sciencecited by 1
  10. 2026Can AI Refute Economic Theory? Evidence from Beyond the Knowledge Cutoffcited by 0
  11. 2026Stable Menus of Public Goods: AI-Enabled Progresscited by 0
  12. 2026Code evolution for link prediction in complex networkscited by 0
11 more
  1. 2026Theoria: Rewrite-Acceptability Verification over Informal Reasoning Statescited by 0
  2. 2026Theoretical Foundations of max@k Reinforcement Learningcited by 0
  3. 2026Xeno-Interpretability: Investigating the Alien Minds of LLMscited by 0
  4. 2026FrontierMath ErdHoscited by 0
  5. 2026When Does Structured Knowledge Help Neural Theorem Proving?cited by 0
  6. 2026TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Sciencecited by 0
  7. 2026GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Researchcited by 0
  8. 2026Distribution Matching Evolutionary Algorithms for Rare Event Samplingcited by 0
  9. 2026LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphscited by 0
  10. 2026The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalizationcited by 0
  11. 2026Do Theorem Provers Need Theorem-Proving Agents? mini-Lean-agent: A Coding-Agent Baseline for Leancited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
  2. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
  3. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
  4. 2026Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
  5. 2024ImProver: Agent-Based Automated Proof Optimization
  6. 2026FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
  7. 2023math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories
  8. 2026ProofCouncil: An LLM Agent for Solving Open Mathematical Problems