A Minimal Agent for Automated Theorem Proving
Borja Requena, Austin Letson, Krystian Nowakowski, Izan Beltran-Ferreiro, Leopoldo Sarra
cs.AI
Feb 27, 2026 · v3
TL;DR
Builds an LLM agent that writes Lean 4 proofs, refining them from compiler feedback and Mathlib search. It is evaluated on Lean benchmarks such as PutnamBench, FATE, and LeanCat.
Abstract
We propose a minimal agentic baseline that enables systematic comparison across different AI-based theorem prover architectures. This design implements the core features shared among state-of-the-art systems: iterative proof refinement, library search and context management. We evaluate this agentic approach using qualitatively different benchmarks and compare various frontier language models and design choices. Our results show competitive performance compared to state-of-the-art approaches, while using a significantly simpler architecture and a fraction of their cost. Additionally, we demonstrate consistent advantages of an iterative approach over multiple single-shot generations, especially in terms of sample efficiency and cost effectiveness. The implementation is released open-source as a candidate reference for future research and as an accessible prover for the community.
Problem
AI theorem provers for Lean are often complex, expensive, and hard to deploy. There is also no simple shared baseline for comparing prover architectures systematically.
Approach
AxProverBase is a minimal modular agent with three parts. A proposer LLM writes Lean code, a review system returns Lean compiler feedback, and a memory module keeps either a history of attempts or a self-reflective context. Optional tools are LeanSearch for Mathlib premise selection and web search. Ablations on a 100-problem PutnamBench subset measure the effect of each component and of different frontier LLMs.
Results
With Claude Opus 4.5 (32k thinking budget, 50 iterations), the agent reaches 54.7% on PutnamBench, 98% on FATE-M, 66% on FATE-H, 24% on FATE-X, and 59% on LeanCat. It is near parity with Hilbert on PutnamBench while using far fewer tokens. Iterative refinement contributes most to performance, followed by memory, then search tools.
| Dataset | Success rate | Avg tokens |
|---|
| PutnamBench | 54.7% | 1.4M |
| LeanCat | 59.0% | 0.6M |
| FATE-M | 98.0% | 55.4k |
| FATE-H | 66.0% | 1.0M |
| FATE-X | 24.0% | 1.3M |
AxProverBase performance and token usage (Opus 4.5, 32k, 50 iterations)
