cs.AIOct 12, 2026
SaveDo Theorem Provers Need Theorem-Proving Agents? mini-Lean-agent: A Coding-Agent Baseline for Lean
Organizations: Princeton Language and Intelligence Princeton University Princeton, NJ 08540 · Department of Mathematics Rutgers University Piscataway, NJ 08854
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.00 | Charge |
|---|---|---|---|---|
| mini-Lean-agent | 0/12 | 4/12 | 7/12 | $14.64 |
| AxProverBase | 0/12 | 0/12 | 4/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.
| Model | Verified | Charge | Calls | Minutes |
|---|---|---|---|---|
| Astra | 12/12 | $15.37 | 106 | 51.3 |
| Fable 5.1 | 11/12 | $120.29 | 133 | 99.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
| Problem | Bash | Search | cat | sed | Python | Lean | Find/list |
|---|---|---|---|---|---|---|---|
| A1 | 63 | 0 | 59 | 0 | 3 | 57 | 0 |
| A2 | 75 | 4 | 62 | 1 | 2 | 61 | 1 |
| A3 | 45 | 1 | 38 | 3 | 0 | 37 | 1 |
| A4 | 79 | 0 | 53 | 1 | 22 | 54 | 1 |
| A5 | 141 | 16 | 68 | 2 | 40 | 66 | 11 |
| A6 | 86 | 5 | 31 | 0 | 49 | 29 | 1 |
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.
| Quantity | mini-Lean-agent | AxProverBase |
|---|---|---|
| Model calls | 1,091 | 724 |
| Uncached input tokens (M) | 6.47 | 8.11 |
| Cached input tokens (M) | 69.69 | 0.78 |
| Visible output tokens (M) | 0.52 | 0.32 |
| Reasoning tokens (M) | 0.70 | 3.64 |
| Cached share of input | 91.5% | 8.7% |
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.
| Problem | mini Verified | mini Charge | Ax Verified | Ax 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 |
Table 5: Per-problem statistics with Gemini and 2 cap on A1, but we mark it correct because no other call was made after the cap was reached.
| Problem | Harness | Verified | Charge | Calls | Hours |
|---|---|---|---|---|---|
| A5 | mini-Lean-agent | ✗ | $10.773974 | 300 | 1.954 |
| A5 | AxProverBase | ✗ | $8.485967 | 300 | 1.653 |
| B6 | mini-Lean-agent | ✗ | $3.268421 | 137 | 0.816 |
| B6 | AxProverBase | ✗ | $6.609995 | 173 | 1.254 |
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.
| Astra | Fable 5.1 | |||||||
|---|---|---|---|---|---|---|---|---|
| Problem | Verified | Charge | Calls | Minutes | Verified | Charge | Calls | Minutes |
| A1 | ✓ | $0.61 | 5 | 3.92 | ✓ | $5.09 | 13 | 9.81 |
| A2 | ✓ | $1.58 | 9 | 6.16 | ✓ | $5.98 | 9 | 12.78 |
| A3 | ✓ | $0.96 | 9 | 8.01 | ✓ | $3.16 | 5 | 10.33 |
| A4 | ✓ | $0.98 | 7 | 6.83 | ✓ | $4.94 | 8 | 11.91 |
| A5 | ✓ | $2.69 | 23 | 17.43 | ✗ | $50.10 | 35 | 40.16 |
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 |
|---|---|---|---|---|---|
| Astra | 10/12 | 12/12 | 12/12 | 12/12 | 12/12 |
| Fable 5.1 | 1/12 | 3/12 | 9/12 | 11/12 | 11/12 |
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.
| Model | Charge |
|---|---|
| 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 |
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.