mlsanityData to 14 Oct 2026

Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs

arXiv 2506.19923 ↗First posted 24 Jun 2025cs.AI cs.LGcited by 31

On the map: LLM agents and tool use → Educational agents and math problem solving

Abstract (arXiv)

We present Prover Agent, a novel AI agent for automated theorem proving that integrates large language models (LLMs) with a formal proof assistant, Lean. Prover Agent coordinates an informal reasoning LLM, a formal prover model, and feedback from Lean while also generating auxiliary lemmas. These auxiliary lemmas are not limited to subgoals in the formal proof but can also include special cases or potentially useful facts derived from the assumptions, which help in discovering a viable proof strategy. It achieves an 88.1% success rate on MiniF2F and solves 25 problems on the PutnamBench with a smaller sample budget than previous approaches, establishing a new state-of-the-art on both benchmarks among methods using small language models (SLMs). We also present theoretical analyses and case studies that illustrate how these generated lemmas contribute to solving challenging problems. Our code is publicly available at https://github.com/kAIto47802/Prover-Agent.

Key facts. Cited by 31 papers in the map (data through 14 Oct 2026). Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use. Builds on 49 of its 81 references that are in the map. First posted on arXiv 24 Jun 2025.

Builds on

49 of 81 references.

Closest ancestors · 1

Same direction, newest first

  1. 2023An In-Context Learning Agent for Formal Theorem-Proving6 Oct

Other references · 48

  1. 2023GPT-4 Technical Reportcited by 18,396
  2. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,459
  3. 2023Direct Preference Optimization: Your Language Model is Secretly a Reward Modelcited by 8,065
  4. 2025DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learningcited by 6,330
  5. 2023Efficient Memory Management for Large Language Model Serving with PagedAttentioncited by 5,944
  6. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
  7. 2022Survey of Hallucination in Natural Language Generationcited by 2,075
  8. 2023A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questionscited by 1,601
  9. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,392
  10. 2024Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvementcited by 1,090
  11. 2023Large Language Models Cannot Self-Correct Reasoning Yetcited by 1,017
  12. 2023Language Agent Tree Search Unifies Reasoning Acting and Planning in Language Modelscited by 574
36 more
  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  2. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  3. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  4. 2024Hallucination is Inevitable: An Innate Limitation of Large Language Modelscited by 332
  5. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  6. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
  7. 2017Thinking Fast and Slow with Deep Learning and Tree Searchcited by 252
  8. 2022HyperTree Proof Search for Neural Theorem Provingcited by 197
  9. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 197
  10. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
  11. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 180
  12. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
  13. 2022Formal Mathematics Statement Curriculum Learningcited by 142
  14. 2024On the Self-Verification Limitations of Large Language Models on Reasoning and Planning Taskscited by 142
  15. 2019The Lean mathematical librarycited by 134
  16. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  17. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  18. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  19. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 122
  20. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
  21. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 84
  22. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 81
  23. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 79
  24. 2025Revisiting the Test-Time Scaling of o1-like Models: Do they Truly Possess Test-Time Scaling Capabilities?cited by 70
  25. 2018Reinforcement Learning of Theorem Provingcited by 69
  26. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 68
  27. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 59
  28. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  29. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Provingcited by 33
  30. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoningcited by 27
  31. 2024Proving Theorems Recursivelycited by 26
  32. 2024LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN provercited by 25
  33. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchicallycited by 22
  34. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoningcited by 18
  35. 2025Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Modelscited by 17
  36. 2024A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problemscited by 6

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 11; 2026: 20.

31 papers.

Sort:

By area:

  1. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
  2. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 60
  3. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 31
  4. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 28
  5. 2025LLM-based Agentic Reasoning Frameworks: A Survey from Methods to Scenarioscited by 26
  6. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 21
  7. 2026A Minimal Agent for Automated Theorem Provingcited by 18
  8. 2025Physics Supernova: AI Agent Matches Elite Gold Medalists at IPhO 2025cited by 14
  9. 2025GenoMAS: A Multi-Agent Framework for Scientific Discovery via Code-Driven Gene Expression Analysiscited by 8
  10. 2026OProver: A Unified Framework for Agentic Formal Theorem Provingcited by 7
  11. 2026Process-Verified Reinforcement Learning for Theorem Proving via Leancited by 7
  12. 2025Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoningcited by 3
19 more
  1. 2025Discovering New Theorems via LLMs with In-Context Proof Learning in Leancited by 2
  2. 2025MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verificationcited by 2
  3. 2026The Origins of Stochasticity: Comprehensive Investigations on Uncertainty Quantification for Large Language Modelscited by 2
  4. 2026Efficient Test-Time Optimization for Multi-Agent Proof Autoformalizationcited by 2
  5. 2026TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflowcited by 1
  6. 2026Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Modelscited by 1
  7. 2026Multi-Modal Multi-Agent Reinforcement Learning for Radiology Report Generationcited by 1
  8. 2026Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4cited by 1
  9. 2026Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalizationcited by 1
  10. 2026Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theorycited by 1
  11. 2026LAMP: Lean-based Agentic framework with MCP and Proof Repaircited by 1
  12. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  13. 2026MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Researchcited by 1
  14. 2026AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Languagecited by 1
  15. 2026Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Proverscited by 0
  16. 2026EULER: Exploring Underused Links with Evidence-Checked Return for Multi-Agent Mathematical Discoverycited by 0
  17. 2026PaperDoctor: Evidence-Grounded and Actionable Feedback for Scientific Papers in Progresscited by 0
  18. 2026SkillEvoLean: Mutation-enhanced skill evolution for Lean proverscited by 0
  19. 2026Let the Library Speak: Self-Advertised Method Selection for Formal Provingcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2024ImProver: Agent-Based Automated Proof Optimization
  2. 2026Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
  3. 2026Advancing Mathematics Research with AI-Driven Formal Proof Search
  4. 2026MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
  5. 2025APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
  6. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
  7. 2026On Reasoning-Centric LLM-based Automated Theorem Proving
  8. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics