Source-linked AI summary
Do Theorem Provers Need Theorem-Proving Agents? mini-Lean-agent: A Coding-Agent Baseline for Lean
Tomas Ortega, Simon Park, Ayush Khaitan, Liam Fowl, Alex Kontorovich, Sanjeev Arora
TL;DR
The paper asks how to distinguish gains from theorem-proving models, harnesses, and specialized tools. It presents a bash-only Lean agent and evaluates it against specialized baselines on Putnam 2025. The agent outperforms AxProverBase with Gemini and solves all twelve problems with Astra at an average cost of $1.28 per problem.
Problem
Specialized Lean harnesses and tools report gains, but it is difficult to attribute them among the base model, harness, and tools.
Source: §1 · p. 2Method
mini-Lean-agent uses bash for repository and Lean work, while a separate trusted evaluator verifies the final artifact in a clean environment.
Source: §1 · p. 2, §2 · pp. 2–3Results
On Putnam 2025, mini-Lean-agent outperforms AxProverBase at lower cost per verified proof and solves all twelve problems with Astra for $1.28 per problem on average.
Source: §5 · p. 5Takeaways & Limitations
The results suggest that a generic coding agent with a minimal harness can serve as a strong baseline for Lean benchmarks.
Source: §5 · p. 5The authors cannot rule out dataset contamination because the tested Astra, Fable, and Gemini versions may have been trained on Putnam 2025 answers.
Source: §4.2 · p. 5
Abstract
from arXiv · showhide
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.
1 Introduction
Lean-agent work often adds specialized harnesses or tools, but reported gains are difficult to attribute among the base model, harness, and tools. mini-Lean-agent is proposed as a practitioner-like baseline to help isolate those contributions.
1 Introduction
- Specialized Lean harnesses and tools report performance gains, but it is difficult to isolate whether they come from the base model, harness, or tools.The paper frames its comparison as generic computer access versus Lean-specific tooling.Source: §1 · p. 2
- mini-Lean-agent uses a deliberately minimal, bash-only interface to establish a baseline closer to general-purpose coding-agent workflows.The motivation is to make base-model contributions easier to separate from specialized scaffolding.Source: §1 · p. 2
- The evaluation asks how much solve rate and cost-efficiency the minimal agent recovers against specialized baselines, and how far stronger models go with the minimal scaffold.These are framed as RQ1 and RQ2, respectively.Source: §1 · p. 2
2 System Design
mini-Lean-agent gives the model bash for repository and Lean work, while a separate trusted evaluator checks its final artifact in a clean environment.
2 System Design
- mini-Lean-agent exposes only bash, through which the model can inspect and edit files, search local libraries, invoke Lean, and manage intermediate work.The model can test intermediate proofs in scratch files before transferring successful work to the target file.Source: §2 · p. 2
- AxProverBase instead provides custom library and web-search tools plus proposer, compiler, and memory modules.The distinction is the kinds of operations models can perform and compose, not simply the number of tools.Source: §2 · p. 2, Figure 1 · p. 3
- A separate evaluator copies the declared artifact into a fresh environment with the original statement and pinned Lean and Mathlib versions, then checks it with Comparator.It rejects undeclared axioms, sorry, admit, build failures, and timeouts.Source: §2 · pp. 2–3
3 Experimental Design
The experiments use Putnam 2025 problems to compare harnesses with the model fixed and to compare models with mini-Lean-agent fixed.
3 Experimental Design
- The evaluation uses the twelve Putnam 2025 challenge files, with Lean 4.28.0-rc1 and Mathlib v4.28.0-rc1 in separate Docker containers.Open-web access and search grounding are disabled.Source: §3 · p. 3
- For the harness comparison, Gemini 3.8 Flash is held fixed across mini-Lean-agent and AxProverBase, with per-problem limits of $2, 200 calls, or 120 active minutes.A5 and B6 receive higher limits of $50, 300 calls, and 24 active hours.Source: §3 · p. 3
- For the model comparison, mini-Lean-agent is held fixed while Astra and Fable 5.1 are run on all twelve problems and compared with Numina’s reported results.The per-problem maximum is $50, 200 calls (300 for A5 and B6), and 24 active hours.Source: §3 · p. 3
4 Results
On Putnam 2025, mini-Lean-agent performs strongly both against AxProverBase with Gemini and with Astra as its base model. Trace and cost analyses describe how the bash-only workflow operates, while the paper notes possible dataset contamination.
4.1 RQ1: A minimal coding agent outperforms a minimal agent with Lean tooling
- 7/12 versus 4/12 runs are verified by mini-Lean-agent and AxProverBase, respectively, with Gemini at a $2 limit.The reported charge per successful run is $2.09 versus $5.24.Source: Table 1 · p. 4, §4.1 · p. 4
- Extra budget on A5 and B6 yields no correct proof for either harness, and the authors cannot rule out dataset contamination.They note that Astra, Fable, and Gemini may have been trained on Putnam 2025 answers.Source: §4.1 · p. 4, §4.2 · p. 5
- All twelve runs use scratch Lean files; across 1,088 requests, 602 combine file writing with Lean invocation, while 73 request rg or grep.In A1, a scratch-file test with exact? leads the model to use Lean’s suggested finite-set lemma in the accepted proof.Source: §4.1 · p. 4
- AxProverBase makes fewer calls than mini-Lean-agent (724 versus 1,091) but generates more reasoning tokens (3.64 million versus 0.70 million).The authors offer more efficient model usage as a possible explanation for the cost difference; cache reads are 91.5% versus 8.7% of input tokens.Source: §4.1 · p. 4
4.2 RQ2: mini-Lean-agent with a strong model is a competitive baseline
- 12/12 Putnam problems are solved with mini-Lean-agent and Astra at an average cost of $1.28 per verified proof.The reported total charge is $15.37; Fable 5.1 verifies 11/12 at $10.94 per verified proof.Source: §4.2 · pp. 4–5, Table 2 · p. 4
5 Conclusion
mini-Lean-agent is a minimal Lean coding-agent baseline whose only model-visible tool is bash. On Putnam 2025, it outperforms AxProverBase at lower cost per verified proof and solves all twelve problems with Astra; the authors suggest it as a strong baseline for Lean benchmarks.
5 Conclusion
- With Astra, mini-Lean-agent solves all twelve Putnam 2025 problems for an average $1.28 per problem.The paper also reports better performance than AxProverBase at lower cost per verified proof.Source: §5 · p. 5
- mini-Lean-agent is a minimal Lean coding-agent baseline whose only model-visible tool is bash.Source: §5 · p. 5
- The authors suggest a generic coding agent with a minimal harness as a strong baseline for Lean benchmarks.Source: §5 · p. 5
- Future work should examine how specialized theorem-proving scaffolding's value changes as base models become more capable.Source: §5 · p. 5
A Supplementary Results
The supplementary results report an unsuccessful Opus 4.5 run and provide qualitative examples and detailed breakdowns of Gemini and other model runs. They also describe model usage, per-problem statistics, and total charges.
A Supplementary Results
- 0/12 problems were solved by mini-Lean-agent with Opus 4.5 under a $5-per-problem budget and 120-minute limit.The authors did not pursue this direction further, noting strong results with more powerful models.Source: A Supplementary Results · p. 7
- On B3, AxProverBase made 40 LeanSearch requests, returned eight proof responses, and made seven memory updates before its final proposal left the non-coprime case open.Two proof responses had unclosed JSON strings, and the proposal retained a sorry block; Figure 2 shows excerpts of this interaction.Source: A Supplementary Results · p. 7, Figure 2 · p. 8
- On A1, Lean suggested Finset.exists_nat_subset_range t in response to a scratch proof, and the accepted proof later used that lemma.Source: A Supplementary Results · p. 8
- Tables 5 and 6 break down Gemini's $2-limit and higher-budget continuation results by problem, while Tables 7 and 8 report Astra and Fable per-problem results and lower-budget thresholds.Source: A Supplementary Results · p. 9, Table 5 · p. 9, Table 6 · p. 9
- Table 9 aggregates model charges across reported experiments, including the twelve unsuccessful Opus 4.5 attempts.Source: A Supplementary Results · p. 9
B Reproducibility
The reproducibility setup pins the benchmark environment and archives experiment artifacts, while the appendix tables specify the scope of per-problem and aggregate cost reporting.
B Reproducibility
- The study pins Lean and Mathlib v4.28.0-rc1, benchmark, harnesses, dependencies, and evaluator, and archives configurations, runs, usage records, and LeanSearch exchanges.Source: B Reproducibility · p. 9
- Proof and evaluator containers have networking disabled, and a fresh independent Comparator verifies each target with a 600-second limit per snapshot.The evaluator rejects incomplete proofs, extra axioms, and metaprogramming, allowing only propext, Quot.sound, and Classical.choice.Source: B Reproducibility · p. 9
- Tables 7 and 8 report Astra and Fable per-problem results at $50 and lower budget limits, while Table 9 aggregates charges over exactly twelve problems per row.The first two rows of Table 9 include higher-budget continuations for A5 and B6.Source: Table 7 · p. 10, Table 8 · p. 10, Table 9 · p. 10
C Prompts
The prompts instruct the model to complete a designated Lean theorem through bash interactions, while preserving the supplied theorem and project setup. They specify a checking-and-revision workflow and strict submission constraints.
C Prompts
- The task requires a complete proof in the fixed target while preserving the supplied statement, source prefix, imports, definitions, and project configuration.Source: C Prompts · p. 11
- Submission must contain no sorry, admit, extra axioms, or metaprogramming, and the final artifact is independently checked in the pinned environment.Source: C Prompts · p. 11
- The model may inspect and edit files, search local libraries, invoke Lean, and create scratch files while working through bash.The prompt recommends checking declaration names in scratch Lean files and running Lean after each proof attempt.Source: C Prompts · pp. 11–12
- The prompt requires a successful check before the agent issues the standalone completion command, after which it cannot continue working.Source: C Prompts · pp. 11–12