mini-Lean-agent：面向 Lean 的编码智能体基线，证明定理证明器是否需要定理证明智能体？

View PDF HTML (experimental)

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.

Comments:	Accepted at the 6th Workshop on Mathematical Reasoning and AI (NeurIPS 2026)
Subjects:	Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)
MSC classes:	68V15
ACM classes:	I.2.3; I.2.8; F.4.1
Cite as:	arXiv:2610.17331 [cs.AI]
	(or arXiv:2610.17331v1 [cs.AI] for this version)
	https://doi.org/10.48550/arXiv.2610.17331 arXiv-issued DOI via DataCite (pending registration)

Submission history

From: Tomàs Ortega [view email]
[v1] Mon, 12 Oct 2026 19:40:30 UTC (35 KB)