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

TL;DR

Prover Agent introduces a modular framework that bridges informal reasoning by LLMs with formal verification in Lean, using auxiliary lemmas to discover viable proof strategies. The approach achieves a new state-of-the-art 88.1% success on MiniF2F with small language models and a small sample budget, validated by theoretical analyses showing lemma-based efficiency gains. Case studies and ablations illustrate how generated lemmas decompose proofs and help uncover strategies, including special-case reasoning and induction, while maintaining Lean verification throughout. The work demonstrates modularity and scalability across prover backbones, with potential to extend to other formal domains beyond mathematics.

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 the MiniF2F benchmark, establishing a new state-of-the-art among methods using small language models (SLMs) with a much lower sample budget than previous approaches. 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.

Figures (4)

• Figure 1: Comparison of theorem-proving performance on the MiniF2F benchmark zheng2021minif2f among methods using SLMs. Our approach achieves a higher success rate with fewer sample budgets, establishing a new state-of-the-art at this scale.
• Figure 2: Overall workflow of Prover Agent. The agent coordinates informal reasoning, formal proving, and Lean verification. It first attempts direct proving; if unsuccessful, it generates auxiliary lemmas to guide the discovery of a viable proof strategy. These lemmas are then formally proved, and the successfully proved lemmas are subsequently used to synthesize the final proof.
• Figure 3: Results for different $N_\mathrm{init}$ and $N_\mathrm{refine}$. The dotted lines indicate that the corresponding sample budget are used in the proof of lemmas.
• Figure 4: Histogram of Lean error counts after $N_\mathrm{init}$.

Theorems & Definitions (16)

• Theorem 4.4: Required Number of Trials
• Theorem 4.5: Threshold Condition for Lemma Efficiency
• Theorem 4.6: Optimal Partition of Lemma Coverage
• Theorem 4.7: Success Probability Improvement by Lemmas
• Lemma C.1: Number of Trials for Success
• proof
• Theorem C.2: Required Number of Trials
• proof
• Theorem C.3: Threshold Condition for Lemma Efficiency
• proof