cs.AIFeb 27, 2026
SaveA Minimal Agent for Automated Theorem Proving
Organizations: Axiomatic AI, Barcelona, Spain.
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.
Figures & tables
Figure 1: Minimal agent for theorem proving. The design focuses on three main aspects: iterative proof refinement, memory system, and access to tools. A proposer agent writes Lean code to prove a given theorem. Then, a compiler verifies if the proposed proof works. If so, it is double-checked by a reviewer agent to prevent any form of cheating. If the code does not compile, or the reviewer objects, the feedback is sent to the memory module, and the cycle starts over with the proposer refining its previous proof informed by the additional context provided by the memory module. In addition, the proposer can be given access to tools such as library search or web search, and call them a fixed number of times before giving its proposal.
Figure 2: Ablation study on different components of the minimal agent . We compare single-shot parallel calls of a general-purpose LLM on its own and embedded within the proposed agentic framework. We show the performance as a function of the number of sampled proofs progressively incorporating elements of the architecture described in Section 3 . Starting by adding a feedback mechanism, we then evaluate two different memory mechanisms (history of previous attempts and a context managed through self-reflection), and we finally incorporate search tools. The entire experiment is conducted with Claude Opus 4.5 with a thinking budget of 10k tokens. The pass@ values are computed out of 50 independent realizations, and we show the 95% confidence interval around them. For the iterative approach, we compute the mean percentage of proven theorems at each iteration and show the standard error of the mean around it. We average over two independent realizations for the different ablations, and three for the full system.
Figure 3: (a) Comparison between LLMs . Claude Sonnet 4.5 and Opus 4.5 have a thinking budget of tokens. Both Gemini 3 Flash and Pro have thinking set to "high". The pass@ are computed from 50 independent proof samples for each model and we show the 95% confidence interval around the obtained value. For the full system, we show the mean performance over 3 full runs up to 50 iterations and show the standard error of the mean. (b) Cost-performance analysis . We compare the performance of different language models as we vary their thinking budget with respect to their cost. We consider thinking budgets of 2k, 10k and 32k tokens for both Claude models, and “low” and “high” for the Gemini models. We also test the “minimal” option for Gemini Flash.
| Model | PutnamBench | FATE-M | FATE-H | FATE-X | LeanCat | |||||
|---|---|---|---|---|---|---|---|---|---|---|
| DeepSeek V2 | 7.1% | @1024 | 25.3% | @1 | 0.4% | @1 | 0.0% | @64 | 9.0% | @32 |
| 62.7% | @64 | 3.0% | @64 | |||||||
| Goedel Prover V2 | 13.0% | @184 | 21.2% | @1 | 0.4% | @1 | 0.0% | @64 | 5.0% | @32 |
| 48.7% | @64 | 2.0% | @64 | |||||||
| Kimina Prover | 1.5% | @192 | 10.5% | @1 | 0.5% | @1 | 0.0% | @64 | 2.0% | @32 |
| 36.0% | @64 | 2.0% | @64 | |||||||
Table 1: Comparison of various AI-based theorem provers with AxProverBase using Claude Opus 4.5 with 32k thinking token budget and 50 iterations. Results for other provers are as reported either in their respective papers or the dataset papers: DeepSeek V2 ( Ren et al., 2025 ) , Goedel Prover V2 ( Lin et al., 2026 ) , Kimina Prover ( Wang et al., 2025a ) , Seed-Prover 1.5 (budget of 10 H20 days / problem) ( Chen et al., 2025a ) , Claude Opus 4.5 (LeanCat evaluation ( Xu et al., 2025 ) ), REAL-Prover ( Shen et al., 2025 ) , Ax-Prover ( Breen et al., 2025 ) , and Hilbert ( Varambally et al., 2026 ) .
Appendix figures & tables8 assets
Supplementary material from the paper’s appendix.
Appendix
| Model | Reference | Solved | Compute Budget |
|---|---|---|---|
| Aleph Prover ($1400 limit) | ( Logical Intelligence, 2026 ) | 668 | Avg $68 |
| Aleph Prover ($400 limit) | ( Logical Intelligence, 2026 ) | 637 | Avg $54 |
| Seed-Prover 1.5 (ByteDance) | ( Chen et al., 2025a ) | 581 | 10 H20 days/problem |
| Aleph Prover ($100 limit) | ( Logical Intelligence, 2026 ) | 500 | Avg $23 |
| Hilbert | ( Varambally et al., 2026 ) | 462 | avg pass@1840 |
| Seed-Prover (ByteDance) | ( Chen et al., 2025b ) | 329 | MEDIUM |
Table 2: PutnamBench Lean Leaderboard (out of 672 problems)
| putnam_1962_a1 | putnam_1962_b6 | putnam_1963_a3 | putnam_1964_a4 |
| putnam_1965_b4 | putnam_1966_a6 | putnam_1966_b6 | putnam_1967_a1 |
| putnam_1968_b5 | putnam_1970_b3 | putnam_1970_b6 | putnam_1972_b4 |
| putnam_1972_b6 | putnam_1973_a3 | putnam_1973_a6 | putnam_1974_a1 |
| putnam_1974_a6 | putnam_1974_b3 | putnam_1974_b6 | putnam_1975_b5 |
| putnam_1976_b3 | putnam_1978_b4 | putnam_1980_a3 | putnam_1980_a6 |
| putnam_1980_b5 | putnam_1981_b1 | putnam_1982_a2 | putnam_1982_b2 |
Table 3: 100 Randomly-Selected PutnamBench Samples for Ablation Studies (Sorted)
Figure 4: Error analysis across multiple ablations . Error distribution for each of the system ablations studied in Section 4.1 : agent with feedback, history of the previous 5 proof attempts, self-managed context based on self-reflection, and the full system with self-reflection and search tools.
Figure 5: Error analysis across multiple underlying LLMs . Error distribution for each of the underlying LLMs studied in Section 4.2 : Gemini 3 Flash, Gemini 3 Pro, Claude 4.5 Sonnet and Claude 4.5 Opus.
| Dataset | Success rate | Max tokens | Avg tokens | Output token % (STD) |
|---|---|---|---|---|
| PutnamBench | 54.7% | 4.2M | 1.4M | 29.7 (6.2) |
| LeanCat | 59.0% | 1.9M | 0.6M | 26.2 (8.1) |
| FATE-M | 98.0% | 1.4M | 55.4k | 28.6 (11.7) |
| FATE-H | 66.0% | 2.8M | 1.0M | 28.5 (4.5) |
| FATE-X | 24.0% | 2.9M | 1.3M | 28.7 (3.7) |
Table 4: Cost statistics for the performance reported in Table 1 . We provide the success rate for the dataset, together with the maximum tokens per problem with which it is obtained before saturating performance, the average tokens per problem within the budget including failed proofs, and the mean ratio between input and output tokens (and its standard deviation across problems).
Figure 6: Cost-performance analysis for the PutnamBench dataset evaluation. On the left, we show the cost-performance Pareto frontier in terms of proof pass rate vs maximum tokens per problem for AxProverBase and Hilbert prover ( Varambally et al., 2026 ) . AxProverBase shows a better scaling than Hilbert, using two orders of magnitude fewer tokens at their highest performance. On the right, we show the distribution of input and output tokens with an average input/output ratio of 2.4.
Figure 7: Cost-performance analysis for the LeanCat dataset evaluation. On the left, we show the cost-performance Pareto frontier in terms of proof pass rate vs maximum tokens per problem. On the right, we show the distribution of input and output tokens, with an average input/output ratio of 2.7.
Figure 8: Cost-performance analysis for the FATE dataset evaluation. Each column corresponds to one of the splits of FATE: M, H, and X from left to right. For each of those, we show (top to bottom): the pass rate vs average tokens per problem, the Pareto frontier of pass rate vs maximum tokens per problem, and the input-output token distributions.