mini-Lean-Agent: A Coding-Agent Baseline for Lean (arxiv.org)

Researchers have introduced the mini-Lean-agent, a streamlined coding agent designed as a benchmark baseline for formal theorem-proving tasks using Lean. Unlike traditional theorem-proving agents that rely on complex, specialized tools, mini-Lean-agent operates with a minimal set of tools, utilizing just bash for repository management and communication with Lean. This simplicity allows for clearer evaluations of performance across various components, aiding in understanding what drives improvements in theorem-proving agents. The significance of mini-Lean-agent lies in its competitive performance against established systems. In tests using the Putnam 2025 benchmark, mini-Lean-agent outperformed AxProverBase, solving 7 out of 12 problems and achieving a remarkable 12 out of 12 with an alternate base model, Astra, at a reduced average cost. These results indicate that even a generic coding agent with minimal tooling can effectively tackle complex theorem-proving challenges, positioning mini-Lean-agent as a valuable standard for future evaluations of theorem-proving infrastructures within the AI/ML community.