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

AI summary

Overview

Research area: Artificial intelligence for mathematics, specifically LLM agents that write formal proofs in the Lean proof assistant.

Technical level: Intermediate. The paper assumes familiarity with benchmark-style evaluation of LLM agents and with the basic idea of formal verification, but it is written at a systems-and-benchmarking level rather than a mathematical one.

Scope: The paper introduces mini-Lean-agent, a deliberately minimal Lean-proving agent whose only model-visible tool is bash, and benchmarks it against specialized theorem-proving harnesses on the Putnam 2025 problem set.

What This Paper Is About

Research on LLM agents for Lean has produced many specialized harnesses and tools, and it is hard to tell whether reported gains come from a better base model, a better harness, or a specific tool. The authors ask whether a generic coding agent with almost no Lean-specific scaffolding can match or beat these specialized systems. They build mini-Lean-agent to test this directly, then compare it against AxProverBase and the reported results of Numina-Lean-Agent.

Key Contributions

1. A minimal baseline agent for Lean. mini-Lean-agent is built on mini-SWE-agent and exposes exactly one tool to the model: bash. The model must inspect and edit the repository, search local libraries, invoke Lean, and manage intermediate work itself, with no purpose-built Lean search or proof-state tools.

2. A separation of agent and verifier. Because the agent can freely modify its own workspace, the output artifact is treated as untrusted. A separate trusted evaluator copies only the declared submission into a fresh environment with the original theorem statement and pinned Lean and Mathlib versions, and uses Comparator (LeanFRO, 2026) to reject undeclared axioms, sorry, admit, build failures, and timeouts.

3. A controlled comparison of generic versus Lean-specific interfaces. For RQ1, the model (Gemini 3.8 Flash with high thinking) and the budget are held fixed while the harness is varied between mini-Lean-agent and AxProverBase. For RQ2, the harness is fixed and the base model is varied across Astra and Fable 5.1.

4. An open baseline and released code. The authors position mini-Lean-agent as a standard baseline for evaluating Lean-proving infrastructure, with code available at https://github.com/TomasOrtega/mini-lean-agent.

Main Findings

• Minimal harness beats specialized tooling at equal budget. With Gemini 3.8 Flash and a $2 per-problem limit, mini-Lean-agent verifies 7/12 Putnam 2025 problems versus AxProverBase's 4/12. Charge per successful run is $2.09 versus $5.24. Total charge across the suite (including unsuccessful attempts) is $14.64 for mini-Lean-agent and $20.97 for AxProverBase.

• The advantage grows at tighter budgets. When output is truncated at a $1.00 per-problem limit, mini-Lean-agent still verifies 4/12 while AxProverBase verifies 0/12. At $0.50, both verify 0/12.

• Extra budget on the hard problems did not help either harness with Gemini. For A5 and B6, running with additional budget (up to $50, 300 calls, and 24 active hours) did not produce a correct proof under either harness.

• A strong model with a minimal harness solves everything. With Astra as the base model, mini-Lean-agent verifies 12/12 problems for $15.37 total, or $1.28 per verified proof, using 106 model calls and 51.3 minutes. Astra solves every problem for under $3, including A5 at $2.69 and B6 at $1.62.

• A second strong model falls one problem short. Fable 5.1 verifies 11/12 for $120.29, or $10.94 per verified proof including the unsuccessful attempt. It leaves only A5 unsolved, reaching $50.10 after 35 calls and 40.16 active minutes while developing an incomplete proof.

• Result is on par with a specialized open-source system, at far lower reported cost. Numina-Lean-Agent is reported as the first open-source system to achieve 12/12 on Putnam 2025. The authors note Numina used Opus 4.5 and report an approximate budget of $50 per task, with $1,000 and 2,040 minutes for A5 and $300 and 797 minutes for B6. The paper states the comparison shows what complete systems achieve but does not isolate harness effects because models and budgets differ.

• Cost difference tracks token and cache behavior. AxProverBase makes fewer model calls (724 versus 1,091) but generates 3.64 million reasoning tokens versus 0.70 million. Cache reads account for 91.5% of mini-Lean-agent's input tokens versus 8.7% for AxProverBase, and memory and review calls account for 11.1% of AxProverBase's charge.

• Bash traces reveal a file-heavy workflow. Of 1,088 requests, 602 combine writing a file with cat and invoking Lean, while only 73 request rg or grep. All twelve runs use scratch Lean files. In A1, the model tests a finite-set lemma with exact? in Scratch.lean and then uses Lean's suggested lemma in the accepted proof.

• Failure modes differ. All 6 unsuccessful AxProverBase runs that exhaust the allowance still leave sorry in their final candidates. On B3, two of eight proof responses truncate mid-JSON and the final candidate leaves a modular-arithmetic case unresolved.

• Contamination cannot be ruled out. The authors state they cannot rule out dataset contamination, since the versions of Astra, Fable, and Gemini used may have been trained on the answers of Putnam 2025.

Methodology in Plain English

The authors take an existing minimal coding agent (mini-SWE-agent) and point it at Lean proof tasks, giving it nothing but a shell. The model reads files, searches the local Mathlib, runs Lean, sees the errors, creates scratch files to test intermediate lemmas, and moves whatever works into the target file. It is also allowed to modify its own working environment.

Because the agent can change its own environment, the authors do not trust its output. After each run, an independent evaluator copies only the declared submission into a clean container with the original theorem statement and the pinned Lean and Mathlib versions, and checks it with Comparator.

The experiments are set up as two controlled comparisons. In the first, the model and budget are fixed while the harness changes, so differences can be attributed to the harness. In the second, the harness is fixed while the base model changes, showing what a minimal scaffold can achieve as models improve. All experiments use the twelve Putnam 2025 challenge files A1–A6 and B1–B6 released with Numina-Lean-Agent, Lean 4.28.0-rc1, and Mathlib v4.28.0-rc1, with open-web access and search grounding disabled. Each problem-agent pair runs in its own Docker container. The standard run limits are $2 model charge, 200 model calls, or 120 minutes of active time; for A5 and B6, and for the stronger-model runs, the limits are raised to $50 model charge, 200 calls (300 for A5 and B6), and 24 active hours per problem.

Why This Matters

The paper's central methodological point is about attribution: when a new Lean-agent system reports gains, it is usually unclear whether the gain comes from the base model, the harness, or a specific tool. By providing a minimal, competitive baseline, mini-Lean-agent gives the field a reference point that makes those gains interpretable. The reported result that a generic coding agent with a shell can reach 12/12 on Putnam 2025 with Astra, at $1.28 per proof, challenges the assumption that specialized theorem-proving scaffolding is necessary for strong benchmark performance.

Real-world applications:

• Mathematicians formalizing research. The paper notes that practitioners already use general-purpose coding agents rather than prover-specific harnesses, so a filesystem-native baseline reflects actual working practice.
• Proof assistant tooling built on top of agents. Systems that help users write Lean proofs can be designed around shell access to the repository rather than a bespoke tool API.
• Benchmark design and leaderboard evaluation. A trusted evaluator using Comparator gives a template for scoring agent output while defending against undeclared axioms, sorry, and statement mutation.
• Cost-aware deployment of coding agents. The per-problem cost figures ($2.09 versus $5.24 per solved problem at equal budget for Gemini; $1.28 with Astra) are directly useful for budgeting agent runs on formal tasks.

Industry relevance is mainly for teams building or procuring coding agents and formal-verification tooling: the paper argues that the marginal value of domain-specific scaffolding should be demonstrated against a generic-shell baseline, not assumed.

Future Directions

• How does the value of specialized scaffolding change as base models improve? The paper's conclusion raises this explicitly as an important question for future work.
• Contamination-free evaluation. The authors flag that they cannot rule out training-data contamination on Putnam 2025, which motivates fresh or held-out benchmarks.
• Isolating harness effects against Numina-Lean-Agent. The current comparison mixes different base models and budgets, so a controlled head-to-head would separate harness contributions from model contributions.
• Why A5 and B6 resist the Gemini configuration. Neither harness produced a correct proof for these problems even with the extended budget, while Astra solved A5 for $2.69 and B6 for $1.62.

Target Audience

Researchers and engineers building Lean agents or formal-verification benchmarks will get the most from this paper, particularly those who need a defensible baseline for measuring whether their specialized tools actually help. It is also useful for practitioners who already drive general-purpose coding agents on Lean repositories, and for evaluators designing trusted verification pipelines for agent-produced proofs.

Authors’ 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.