cs.AIOct 12, 2026

Do Theorem Provers Need Theorem-Proving Agents? mini-Lean-agent: A Coding-Agent Baseline for Lean

Authors: Tomas Ortega, Simon Park, Ayush Khaitan, Liam Fowl, Alex Kontorovich, Sanjeev Arora

Organizations: Princeton Language and Intelligence Princeton University Princeton, NJ 08540 · Department of Mathematics Rutgers University Piscataway, NJ 08854

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

General-purpose coding agents use standard shell and file interactions, yet formal theorem-proving agents often rely on specialized, ad-hoc tooling. This makes it difficult to determine which components of theorem-proving agents provide benchmark gains: an improved base model, a specialized harness, a specific tool, or a combination of any of them. We introduce mini-Lean-agent, a deliberately minimal agent for Lean tasks whose only model-visible tool is bash. The model must use bash to inspect and edit the repository, search local libraries, invoke Lean, and manage its own intermediate work, while a separate trusted evaluator verifies the final artifact. We compare mini-Lean-agent against AxProverBase and Numina-Lean-Agent on the Putnam 2025 benchmark. Experiments with Gemini 3.8 Flash as the base model show that mini-Lean-agent solves 7/12 problems at $2 per problem limit, compared with AxProverBase's 4/12. With Astra as the base model, mini-Lean-agent solves 12/12 problems at an average cost of $1.28 per problem. This suggests that a generic coding agent with a minimal harness can already achieve strong performance on Lean benchmarks. Our results motivate using mini-Lean-agent as a standard baseline when evaluating theorem-proving infrastructure.

Figures & tables

Figure 1: A comparison between mini-Lean-agent and AxProverBase workflow. mini-Lean-agent is only given bash tools, through which it can directly search for local Mathlib statements and edit files containing the target proof. AxProverBase instead introduces customized search tools and specialized modules in the workflow.
Harness$0.50$1.00$2.00Charge
mini-Lean-agent0/124/127/12$14.64
AxProverBase0/120/124/12$20.97
Table 1: Comparison between mini-Lean-agent and AxProverBase with Gemini at $2 limit. Each column (except last) shows the number of verified problems out of 12 when the output is truncated at an even smaller per-problem limit. The last column shows the total charge, including that for unsuccessful attempts. This does not include the charge for the higher budget run for A5/B6.
ModelVerifiedChargeCallsMinutes
Astra12/12$15.3710651.3
Fable 5.111/12$120.2913399.9
Table 2: Performance of mini-Lean-agent with Astra and Fable at $50 limit. The total charge includes the charge for unsuccessful attempts.
Appendix figures & tables7 assets

Supplementary material from the paper’s appendix.

Appendix

ProblemBashSearchcatsedPythonLeanFind/list
A16305903570
A27546212611
A34513830371
A479053122541
A514116682406611
A686531049291
Appendix
Table 3: Number of tools requested through bash by mini-Lean-agent with Gemini and $2 limit. The first column (bash) includes all requests, including malformed ones. “Search” refers commands like rg and grep . “Lean” refers to commands like lake env lean or lake build . Some tools may be counted in more than one column: e.g., a request can write a file with cat and invoke Lean.
Quantitymini-Lean-agentAxProverBase
Model calls1,091724
Uncached input tokens (M)6.478.11
Cached input tokens (M)69.690.78
Visible output tokens (M)0.520.32
Reasoning tokens (M)0.703.64
Cached share of input91.5%8.7%
Appendix
Table 4: Model usage of mini-Lean-agent and AxProverBase with Gemini and $2 limit. Token counts sum across requests, including repeated context. Cache percentages use all input tokens as the denominator. Model calls include requests that return no bash action.
Problemmini Verifiedmini ChargeAx VerifiedAx Charge
A1✓$0.518454✓$2.001509
A2✓$0.658883✗$0.141243
A3✓$0.677093✓$1.758844
A4✓$1.064088✗$2.014457
A5✗$2.042195✗$2.000157
A6✓$1.192095✗$1.949676
Appendix
Table 5: Per-problem statistics with Gemini and 2limit.Thisprovidesadetailedbreakdownoftheaggregateresultsin\seqifin:NeFenglishnamesep=,pairsep=and,listsep=,,lastsep=and,tpairsep=and,tlistsep=,,tlastsep=,and,notesep=,rangesep=to,type=book,Name−sg=Book,name−sg=book,Name−pl=Books,name−pl=books,type=part,Name−sg=Part,name−sg=part,Name−pl=Parts,name−pl=parts,type=chapter,Name−sg=Chapter,name−sg=chapter,Name−pl=Chapters,name−pl=chapters,type=section,Name−sg=Section,name−sg=section,Name−pl=Sections,name−pl=sections,type=paragraph,Name−sg=Paragraph,name−sg=paragraph,Name−pl=Paragraphs,name−pl=paragraphs,Name−sg−ab=Par.,name−sg−ab=par.,Name−pl−ab=Par.,name−pl−ab=par.,type=appendix,Name−sg=Appendix,name−sg=appendix,Name−pl=Appendices,name−pl=appendices,type=page,Name−sg=Page,name−sg=page,Name−pl=Pages,name−pl=pages,rangesep=–,rangetopair=false,type=line,Name−sg=Line,name−sg=line,Name−pl=Lines,name−pl=lines,type=figure,Name−sg=Figure,name−sg=figure,Name−pl=Figures,name−pl=figures,Name−sg−ab=Fig.,name−sg−ab=fig.,Name−pl−ab=Figs.,name−pl−ab=figs.,type=table,Name−sg=Table,name−sg=table,Name−pl=Tables,name−pl=tables,type=item,Name−sg=Item,name−sg=item,Name−pl=Items,name−pl=items,type=footnote,Name−sg=Footnote,name−sg=footnote,Name−pl=Footnotes,name−pl=footnotes,type=endnote,Name−sg=Note,name−sg=note,Name−pl=Notes,name−pl=notes,type=note,Name−sg=Note,name−sg=note,Name−pl=Notes,name−pl=notes,type=equation,Name−sg=Equation,name−sg=equation,Name−pl=Equations,name−pl=equations,Name−sg−ab=Eq.,name−sg−ab=eq.,Name−pl−ab=Eqs.,name−pl−ab=eqs.,refbounds−first−sg=,(,),,refbounds=(,,,),type=theorem,Name−sg=Theorem,name−sg=theorem,Name−pl=Theorems,name−pl=theorems,type=lemma,Name−sg=Lemma,name−sg=lemma,Name−pl=Lemmas,name−pl=lemmas,type=corollary,Name−sg=Corollary,name−sg=corollary,Name−pl=Corollaries,name−pl=corollaries,type=proposition,Name−sg=Proposition,name−sg=proposition,Name−pl=Propositions,name−pl=propositions,type=definition,Name−sg=Definition,name−sg=definition,Name−pl=Definitions,name−pl=definitions,type=proof,Name−sg=Proof,name−sg=proof,Name−pl=Proofs,name−pl=proofs,type=result,Name−sg=Result,name−sg=result,Name−pl=Results,name−pl=results,type=remark,Name−sg=Remark,name−sg=remark,Name−pl=Remarks,name−pl=remarks,type=example,Name−sg=Example,name−sg=example,Name−pl=Examples,name−pl=examples,type=algorithm,Name−sg=Algorithm,name−sg=algorithm,Name−pl=Algorithms,name−pl=algorithms,type=listing,Name−sg=Listing,name−sg=listing,Name−pl=Listings,name−pl=listings,type=exercise,Name−sg=Exercise,name−sg=exercise,Name−pl=Exercises,name−pl=exercises,type=solution,Name−sg=Solution,name−sg=solution,Name−pl=Solutions,name−pl=solutions\seqgputright:Neenglish\msginfo:nnezref−cleverlangfile−loadedenglish\tlputleft:Ne??.“mini”referstomini−Lean−agentand“Ax”referstoAxProverBase.ThetotalchargedoesnotincludethechargeforthehigherbudgetrunforA5/B6.NotethatAxProverBasespentslightlyoverthe2 limit. This provides a detailed breakdown of the aggregate results in \seq_if_in:NeF englishnamesep= ,pairsep= and ,listsep=, ,lastsep= and ,tpairsep= and ,tlistsep=, ,tlastsep=, and ,notesep= ,rangesep= to ,type=book,Name-sg=Book,name-sg=book,Name-pl=Books,name-pl=books,type=part,Name-sg=Part,name-sg=part,Name-pl=Parts,name-pl=parts,type=chapter,Name-sg=Chapter,name-sg=chapter,Name-pl=Chapters,name-pl=chapters,type=section,Name-sg=Section,name-sg=section,Name-pl=Sections,name-pl=sections,type=paragraph,Name-sg=Paragraph,name-sg=paragraph,Name-pl=Paragraphs,name-pl=paragraphs,Name-sg-ab=Par.,name-sg-ab=par.,Name-pl-ab=Par.,name-pl-ab=par.,type=appendix,Name-sg=Appendix,name-sg=appendix,Name-pl=Appendices,name-pl=appendices,type=page,Name-sg=Page,name-sg=page,Name-pl=Pages,name-pl=pages,rangesep=–,rangetopair=false,type=line,Name-sg=Line,name-sg=line,Name-pl=Lines,name-pl=lines,type=figure,Name-sg=Figure,name-sg=figure,Name-pl=Figures,name-pl=figures,Name-sg-ab=Fig.,name-sg-ab=fig.,Name-pl-ab=Figs.,name-pl-ab=figs.,type=table,Name-sg=Table,name-sg=table,Name-pl=Tables,name-pl=tables,type=item,Name-sg=Item,name-sg=item,Name-pl=Items,name-pl=items,type=footnote,Name-sg=Footnote,name-sg=footnote,Name-pl=Footnotes,name-pl=footnotes,type=endnote,Name-sg=Note,name-sg=note,Name-pl=Notes,name-pl=notes,type=note,Name-sg=Note,name-sg=note,Name-pl=Notes,name-pl=notes,type=equation,Name-sg=Equation,name-sg=equation,Name-pl=Equations,name-pl=equations,Name-sg-ab=Eq.,name-sg-ab=eq.,Name-pl-ab=Eqs.,name-pl-ab=eqs.,refbounds-first-sg=,(,),,refbounds=(,,,),type=theorem,Name-sg=Theorem,name-sg=theorem,Name-pl=Theorems,name-pl=theorems,type=lemma,Name-sg=Lemma,name-sg=lemma,Name-pl=Lemmas,name-pl=lemmas,type=corollary,Name-sg=Corollary,name-sg=corollary,Name-pl=Corollaries,name-pl=corollaries,type=proposition,Name-sg=Proposition,name-sg=proposition,Name-pl=Propositions,name-pl=propositions,type=definition,Name-sg=Definition,name-sg=definition,Name-pl=Definitions,name-pl=definitions,type=proof,Name-sg=Proof,name-sg=proof,Name-pl=Proofs,name-pl=proofs,type=result,Name-sg=Result,name-sg=result,Name-pl=Results,name-pl=results,type=remark,Name-sg=Remark,name-sg=remark,Name-pl=Remarks,name-pl=remarks,type=example,Name-sg=Example,name-sg=example,Name-pl=Examples,name-pl=examples,type=algorithm,Name-sg=Algorithm,name-sg=algorithm,Name-pl=Algorithms,name-pl=algorithms,type=listing,Name-sg=Listing,name-sg=listing,Name-pl=Listings,name-pl=listings,type=exercise,Name-sg=Exercise,name-sg=exercise,Name-pl=Exercises,name-pl=exercises,type=solution,Name-sg=Solution,name-sg=solution,Name-pl=Solutions,name-pl=solutions \seq_gput_right:Ne english \msg_info:nne zref-cleverlangfile-loadedenglish \tl_put_left:Ne ?? . “mini” refers to mini-Lean-agent and “Ax” refers to AxProverBase. The total charge does not include the charge for the higher budget run for A5/B6. Note that AxProverBase spent slightly over the 2 cap on A1, but we mark it correct because no other call was made after the cap was reached.
ProblemHarnessVerifiedChargeCallsHours
A5mini-Lean-agent✗$10.7739743001.954
A5AxProverBase✗$8.4859673001.653
B6mini-Lean-agent✗$3.2684211370.816
B6AxProverBase✗$6.6099951731.254
Appendix
Table 6: Per-problem statistics with Gemini and a higher limit on A5 and B6. Each result includes the model charge for the first $2 portion of the model output, where they continued from. If the final proof attempt was unsuccessful, the agent may stop before reaching any of the three limits.
 AstraFable 5.1
ProblemVerifiedChargeCallsMinutesVerifiedChargeCallsMinutes
A1✓$0.6153.92✓$5.09139.81
A2✓$1.5896.16✓$5.98912.78
A3✓$0.9698.01✓$3.16510.33
A4✓$0.9876.83✓$4.94811.91
A5✓$2.692317.43✗$50.103540.16
Appendix
Table 7: Per-problem statistics of mini-Lean-agent with Astra and Fable 5.1 at $50 limit. This provides a detailed breakdown of the aggregate results in \seq_if_in:NeF englishnamesep= ,pairsep= and ,listsep=, ,lastsep= and ,tpairsep= and ,tlistsep=, ,tlastsep=, and ,notesep= ,rangesep= to ,type=book,Name-sg=Book,name-sg=book,Name-pl=Books,name-pl=books,type=part,Name-sg=Part,name-sg=part,Name-pl=Parts,name-pl=parts,type=chapter,Name-sg=Chapter,name-sg=chapter,Name-pl=Chapters,name-pl=chapters,type=section,Name-sg=Section,name-sg=section,Name-pl=Sections,name-pl=sections,type=paragraph,Name-sg=Paragraph,name-sg=paragraph,Name-pl=Paragraphs,name-pl=paragraphs,Name-sg-ab=Par.,name-sg-ab=par.,Name-pl-ab=Par.,name-pl-ab=par.,type=appendix,Name-sg=Appendix,name-sg=appendix,Name-pl=Appendices,name-pl=appendices,type=page,Name-sg=Page,name-sg=page,Name-pl=Pages,name-pl=pages,rangesep=–,rangetopair=false,type=line,Name-sg=Line,name-sg=line,Name-pl=Lines,name-pl=lines,type=figure,Name-sg=Figure,name-sg=figure,Name-pl=Figures,name-pl=figures,Name-sg-ab=Fig.,name-sg-ab=fig.,Name-pl-ab=Figs.,name-pl-ab=figs.,type=table,Name-sg=Table,name-sg=table,Name-pl=Tables,name-pl=tables,type=item,Name-sg=Item,name-sg=item,Name-pl=Items,name-pl=items,type=footnote,Name-sg=Footnote,name-sg=footnote,Name-pl=Footnotes,name-pl=footnotes,type=endnote,Name-sg=Note,name-sg=note,Name-pl=Notes,name-pl=notes,type=note,Name-sg=Note,name-sg=note,Name-pl=Notes,name-pl=notes,type=equation,Name-sg=Equation,name-sg=equation,Name-pl=Equations,name-pl=equations,Name-sg-ab=Eq.,name-sg-ab=eq.,Name-pl-ab=Eqs.,name-pl-ab=eqs.,refbounds-first-sg=,(,),,refbounds=(,,,),type=theorem,Name-sg=Theorem,name-sg=theorem,Name-pl=Theorems,name-pl=theorems,type=lemma,Name-sg=Lemma,name-sg=lemma,Name-pl=Lemmas,name-pl=lemmas,type=corollary,Name-sg=Corollary,name-sg=corollary,Name-pl=Corollaries,name-pl=corollaries,type=proposition,Name-sg=Proposition,name-sg=proposition,Name-pl=Propositions,name-pl=propositions,type=definition,Name-sg=Definition,name-sg=definition,Name-pl=Definitions,name-pl=definitions,type=proof,Name-sg=Proof,name-sg=proof,Name-pl=Proofs,name-pl=proofs,type=result,Name-sg=Result,name-sg=result,Name-pl=Results,name-pl=results,type=remark,Name-sg=Remark,name-sg=remark,Name-pl=Remarks,name-pl=remarks,type=example,Name-sg=Example,name-sg=example,Name-pl=Examples,name-pl=examples,type=algorithm,Name-sg=Algorithm,name-sg=algorithm,Name-pl=Algorithms,name-pl=algorithms,type=listing,Name-sg=Listing,name-sg=listing,Name-pl=Listings,name-pl=listings,type=exercise,Name-sg=Exercise,name-sg=exercise,Name-pl=Exercises,name-pl=exercises,type=solution,Name-sg=Solution,name-sg=solution,Name-pl=Solutions,name-pl=solutions \seq_gput_right:Ne english \msg_info:nne zref-cleverlangfile-loadedenglish \tl_put_left:Ne ?? . Only Fable reaches its model charge limit on A5.
Model$2$5$10$20$50
Astra10/1212/1212/1212/1212/12
Fable 5.11/123/129/1211/1211/12
Appendix
Table 8: Per-problem statistics of mini-Lean-agent with Astra and Fable 5.1 at a lower budget limit. Each column shows the number of verified problems out of 12 when the output is truncated at an even smaller per-problem limit.
ModelCharge
Gemini 3.8 Flash$24.612816
Gemini 3.8 Flash (AxProverBase)$32.067014
Opus 4.5$61.596995
Astra$15.367271
Fable 5.1$120.294990
Total$253.939087
Appendix
Table 9: Total model charge. Except for the second row, mini-Lean-agent is the harness used. Each row aggregates the model charge for exactly twelve problems. The first two rows include the higher budget continuations for A5 and B6.
More in this topic

Large Language Model-Guided Theorem Proving

See all 40 papers

Explore similar work

CardsList
May 26, 2026

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving

MerLean-Prover is an end-to-end Lean4 theorem prover that replaces sorry declarations with kernel-checkable proofs. It is built from three agent types (Planning, Check, and Lean) composed by a recursive outer loop whose unit of revision is the proof plan itself, and uses no fine-tuning, no custom RL objective, and no theorem-specific scaffolding. On FormalQualBench, a benchmark of 23 PhD-qualifying-exam theorems, MerLean-Prover solves 10/23, surpassing the strongest published open-source baseline (OpenGauss, 8/23). On Putnam2025, the same harness closes 12/12 with substantially lower total wall-clock than the next-best system that closes the full set. The harness also transfers to smaller models: Sonnet closes all four tested FormalQualBench problems, and Haiku closes the two short ones. These results suggest that harness design is a central factor in end-to-end Lean4 theorem proving, alongside raw model capability, and that a relatively simple harness can already be effective.

Jinzheng Li, Zeru Zhu, Yuanjie Ren

1Northeastern University · 2Stony Brook University · 3Massachusetts Institute of Technology

Large Language Model-Guided Theorem ProvingAutomated Theorem ProvingLean Theorem Proving
AskPDF
Jun 3, 2026

Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean

Large language models (LLMs) are increasingly used in workflows for generating formal proofs in Lean. These workflows often decompose problems into smaller lemmas, sample many proof attempts, and use compiler feedback to guide search. However, they can be prohibitively expensive, often spending substantial compute on attempts that ultimately fail. In this work, we address this problem with an action routing agent that consists of a data plane and a control plane. The data plane generates natural-language lemma decompositions, formalizes them in Lean, and samples proof attempts for the resulting theorem and lemma targets. The control plane observes previous failed Lean attempts, estimates both the likelihood of success and the cost of another attempt, and decides whether to continue proving the current target or restart from a new breakdown. On a subset of PutnamBench, our agent decreases the cost by 28.9% over a fixed-step baseline on average, preserving performance while using substantially less compute. These results suggest that failed Lean trajectories provide actionable signals for cost-aware resource allocation in agentic theorem proving.

Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck +1

1ETH Zurich, Switzerland.

Automated Theorem ProvingLean Theorem Proving
AskPDF
Oct 1, 2026

FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification

Coding agents increasingly automate Lean proof development, but successful compilation alone does not establish that a candidate proves the intended statement under acceptable assumptions. We present FORALL-LEAN-AGENT, a frontend-agnostic framework for auditable reasoning in formal mathematics and software verification. The framework combines isolated workspaces, Lean tools, and fresh review with statement comparison, axiom audits, and independent proof checking where supported. Verification evidence and reviewer decisions are bound to the same candidate artifact, making acceptance traceable. We evaluate the framework on VeriSoftBench, PutnamBench, and both problems in the Lean Eval softwareverification track. On the 100-task VeriSoftBench subset, integration with FORALLLEAN-AGENT raises benchmark-rule success from 93 to 100 for GPT-5.6 Sol at low effort while reducing cost from 69to69 to 62. The PutnamBench evaluation accepts all 672 problems at an average of $4.72 each. These results show that agent harness design can improve correctness and efficiency while providing evidence beyond aggregate solve counts.

Naing Oo Lwin

Astrio Labs

AI Agent AuditingFormal VerificationLLM Agent VerificationLean Theorem Proving
AskPDF