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

arXiv:2610.17331v1 Announce Type: new 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.

Related

• FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification
• LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
• ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers
• FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
• Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement

Source: arXiv cs.AI | 2026-10-15