![[2506.19923] Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs](https://arxiv.org/static/browse/0.3.4/images/arxiv-logo-fb.png){kind=logo}
[2506.19923] Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
Summary
The paper introduces Prover Agent, an AI framework that combines large language models with formal proof assistants to enhance automated theorem proving, achieving state-of-the-art results.
Why It Matters
This research is significant as it addresses the growing need for effective automated reasoning tools in mathematics and computer science. By integrating LLMs with formal proof systems, Prover Agent could streamline the process of theorem proving, making it more accessible and efficient, which is crucial for advancing AI capabilities in formal reasoning.
Key Takeaways
- Prover Agent integrates LLMs with the Lean proof assistant for enhanced theorem proving.
- Achieves an 88.1% success rate on MiniF2F and sets a new benchmark on PutnamBench.
- Generates auxiliary lemmas that aid in discovering viable proof strategies.
- Includes theoretical analyses and case studies demonstrating the framework's effectiveness.
- Publicly available code encourages further research and application in the field.
Computer Science > Artificial Intelligence arXiv:2506.19923 (cs) [Submitted on 24 Jun 2025 (v1), last revised 17 Feb 2026 (this version, v5)] Title:Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs Authors:Kaito Baba, Chaoran Liu, Shuhei Kurita, Akiyoshi Sannai View a PDF of the paper titled Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs, by Kaito Baba and 3 other authors View PDF Abstract: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 this https URL. Comments: Subjects: Artificial Intelligence (cs.AI); Machine Learning (cs.LG) Cite as: arXiv:2506.19923 [cs.AI] (o...
