PaperlayerView exact revision on arXiv

Source-linked AI summary

A Minimal Agent for Automated Theorem Proving

Borja Requena, Austin Letson, Krystian Nowakowski, Izan Beltran-Ferreiro, Leopoldo Sarra

arXiv:2602.24273v3cs.AI

TL;DR

Automated theorem proving can support verifiable scientific reasoning, but formal methods remain underused despite their broad applicability. This paper introduces AxProverBase, a minimal modular agent combining iterative proof refinement, memory, compiler feedback, and search; it achieves competitive performance across diverse formal domains with substantially better cost-performance tradeoffs than more elaborate systems.

  • Problem

    Formal methods can rigorously validate arguments and conclusions, yet they remain underused despite broad applicability across scientific and engineering domains.

  • Method

    AxProverBase is a modular theorem-proving agent that combines iterative proof refinement, memory, compiler-based review, and search tools for independently testable ablations.

  • Results

    AxProverBase reaches 54.7% on PutnamBench at pass@1 and remains competitive across qualitatively different formal domains while using a substantially simpler architecture and lower token budgets.

  • Takeaways & Limitations

    Its simplicity and modularity make AxProverBase an accessible practical prover and a moving baseline for separating architectural gains from improvements in foundation models.

  • Takeaways & Limitations

    Proof certification remains relative to the formal statement, dependencies, and trusted kernel, so misformalization, benchmark overfitting, or overreliance on automated outputs can cause misplaced confidence.

Abstract

from arXiv · show

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.

1. Introduction

Automated theorem proving can support verifiable scientific reasoning, but existing systems make it difficult to separate architectural gains from improvements in foundation models. The paper introduces AxProverBase, a minimal modular agent centered on iterative refinement, memory, and search, and reports competitive results with a simpler design.

  • Automated theorem proving formalizes arguments as theorems whose proofs can certify correctness without human intervention.
  • Existing provers combine complex components such as reinforcement learning, proof-trace supervision, recursive decomposition, and multiple tools.
  • Rapid improvements in Lean, Mathlib, and general-purpose LLMs make it difficult to distinguish architectural innovation from stronger underlying models.
  • AxProverBase isolates iterative proof refinement, context management, search, and base-model choice in a modular architecture suitable for ablation studies.
  • Iterative proof refinement is reported as the largest performance factor and alone can outperform many complex state-of-the-art approaches.
  • Memory reduces errors, search tools help less strongly, and more capable models benefit most from appropriate scaffolding.
  • Simple agents such as AxProverBase achieve competitive cross-domain results and are positioned as accessible options for practical use.

2. Related work

Automated theorem-proving research spans tree-search and whole-proof systems, increasingly combining retrieval, decomposition, feedback, and specialized training. The paper positions its minimal agent against these elaborate approaches while evaluating domains beyond competition mathematics.

  • Tree-search methods construct proofs line by line while interacting with Lean, whereas whole-proof methods generate complete proofs and increasingly use iterative compiler-feedback loops.
  • AlphaProof, REAL-Prover, and related systems illustrate advances from recursive proof construction and semantic theorem retrieval.
  • Recent systems address sparse correct-proof data through self-play, synthetic curricula, theorem decomposition, and reinforcement-learning supervision.
  • Hilbert combines informal reasoning, theorem retrieval, specialized Lean generation, verifier feedback, and recursive proof construction.
  • Seed Prover integrates iterative refinement, compiler feedback, library search, decomposition, context management, and a geometry engine.
  • Ax-Prover shows that a general-purpose model with tools and iterative proof development can outperform specialized provers and generalize beyond competition mathematics.
  • Benchmarks include MiniF2F and PutnamBench from formalized competitions, while FATE targets abstract and commutative algebra at multiple difficulty levels.

3. Architecture

AxProverBase uses a modular loop in which a proposer generates Lean code, verification returns concrete feedback, and memory informs later attempts. Optional library and web search provide additional context before proposal generation.

  • The architecture has three core features: iterative feedback, memory across attempts, and tools for searching information needed to complete proofs.
  • The proposer receives the target theorem, its context, and prior attempts, then generates Lean code to complete the proof.
  • A ReAct-style proposer may make one parallel round of tool calls before producing a proof.
  • Library search uses LeanSearch and vector embeddings to select relevant premises from Mathlib.
  • Web search is enabled because compiling Lean code is treated as the practical bottleneck rather than informal reasoning.
  • The review system combines deterministic compilation checks with an LLM reviewer that flags preserved-statement violations and potential cheating mechanisms.
  • Memory may retain no history, recent full attempts, or a self-managed reflective context that preserves lessons while limiting context growth.

4. Experiments

Experiments build AxProverBase incrementally, measuring feedback, memory, tools, and foundation-model effects through ablations, cost analysis, and benchmark comparisons. Iterative refinement and memory improve sample efficiency, while the complete minimal agent achieves competitive theorem-proving performance with substantially lower resource use.

  • Bottom-up system analysis: Ablations progressively add feedback, memory, and search tools to a bottom-up agent architecture evaluated on a 100-sample PutnamBench subset.The study uses this subset to reduce cost while enabling more experiments and to limit overfitting to a particular target dataset.
  • Bottom-up system analysis: Single-shot sampling is inefficient: increasing k helps mainly on easier theorems, while difficult theorems are rarely proven.The pass@k strategy generates independent proofs without feedback, tools, or memory.
  • Bottom-up system analysis: Iterative refinement yields the largest performance gain, but its returns diminish as iterations increase because the simple approach can repeat past errors.Feedback informs subsequent iterations about errors from failed proof attempts.
  • Bottom-up system analysis: Longer-term memory improves on immediate refinement by reducing Lean errors and helping the agent address open goals across more iterations.The evaluated mechanisms store the previous 5 attempts or maintain a self-managed context.
  • Bottom-up system analysis: Search tools target errors from misidentifying or misusing Mathlib theorems and tactics, and their addition produces the best performance in the component analysis.The system uses LeanSearch for Mathlib and Tavily for internet search.
  • Foundation model comparison: Within the agentic framework, all models improve over stand-alone generation, with stronger models gaining relatively larger improvements.Claude models prove about three times as many theorems as Gemini counterparts, while higher thinking budgets generally increase both cost and performance.
  • Benchmark dataset evaluations: High FATE and LeanCat scores suggest applicability to realistic research scenarios, and no dedicated training or fine-tuning is required for different Lean and Mathlib versions.The paper presents this as an indication that the system can prove a large portion of theorems in complex projects.

5. Discussion

AxProverBase shows that a simple, modular theorem-proving agent can achieve strong cross-domain performance efficiently, while iterative refinement and memory provide the largest gains. Its moving-baseline role supports separating improvements from stronger models from genuine architectural advances.

  • Performance: 54.7% on PutnamBench, 98.0% on FATE-M, 66.0% on FATE-H, 24.0% on FATE-X, and 59.0% on LeanCat demonstrate broad performance without domain-specific fine-tuning.The system remains competitive with more elaborate prover architectures despite its simpler design.
  • Efficiency: 12.6$ average cost per sample accompanies near-parity with Hilbert on PutnamBench: 54.7% versus 55.9%.AxProverBase used 4.2M tokens per problem versus Hilbert’s 1880.4M, and achieved better token efficiency on FATE.
  • Ablations: Iterative refinement is the main performance driver, while memory provides the second-largest gain and search tools contribute a smaller improvement.Memory mechanisms and tools reduce code errors; name and syntax errors drop by 53% and 26%, respectively.
  • Model dependence: Stronger models benefit more from the same architecture, so the agentic framework amplifies rather than removes dependence on the underlying model.For Claude Opus, increasing the thinking budget from 10k to 32k tokens matches doubling iterations at significantly lower cost.
  • Future use: AxProverBase’s modular design supports low-cost experimentation and component-level improvements, including richer retrieval, stronger verification, and better memory management.The framework is intended to be both a practical prover and an interpretable research platform.
  • Reference baseline: As frontier models improve, AxProverBase improves with them and provides a moving reference for distinguishing model gains from architectural innovation.The implementation and evaluation infrastructure are open sourced to support reproducible comparison and future extension.

Impact Statement

The paper frames automated theorem proving as a route to machine-checkable scientific reasoning, while emphasizing that formal verification remains bounded by faithful formalization and human oversight. Its implementation uses iterative Lean proof development supported by compiler feedback, memory, search, and structured prompts.

  • Impact: Automated theorem proving can certify formalized arguments and conclusions without human intervention, supporting verifiable scientific reasoning.The paper connects this potential to validation and broader scientific and engineering workflows.
  • Limitations: Proof-assistant certification is relative to the formal statement, dependencies, and trusted kernel, and does not ensure faithful representation of the intended scientific claim.The paper identifies misformalization, benchmark overfitting, and overreliance on automation as risks requiring human oversight.
  • Iterative proof process: The iterative proposer receives the Lean file, target theorem, recent attempt, and available memory context, then uses compiler feedback to guide subsequent proof development.The prompt requires preserving the theorem statement while changing only the proof body.
  • Iterative proof process: Incomplete proofs and `sorry` statements are used diagnostically so compilation exposes unsolved goals and errors for later iterations.The process treats build feedback as information rather than as a final proof result.
  • Iterative proof process: The prompts instruct the agent to retain lessons from previous attempts, fix existing errors, complete missing proof parts, and explore alternatives when needed.Later iterations focus on analyzing feedback and addressing issues directly.
  • Output design: The proof output is structured into imports, opened namespaces, and an updated theorem containing the revised proof.The format also requires Lean tactics, applicable Mathlib lemmas, and necessary imports.
  • Examples: The examples progress from an exploratory tactic attempt through incomplete induction, goal closure, and correction of an invalid lemma name.The final example uses `omega` after compiler feedback identifies the `Nat.add_succ` error.

C. Example: complete proof process

The complete proof-process example uses a real FATE-M problem to illustrate why AxProverBase may require iterative refinement rather than succeeding on its first attempt. It presents the architecture’s inputs and outputs while omitting fixed system prompts.

  • Example scope: The example provides all inputs and outputs of the main architecture components while omitting fixed system prompts for simplicity.It is intended as a concrete proof-generation process example tied to an evaluated problem.
  • Example selection: The example uses problem 116 from FATE-M, which asks for an identity proof in a non-commutative ring.The problem was selected for broad understandability and because the evaluated agent needed a second iteration to finish it.

C.1. First iteration

The first iteration proposes a proof using a helper equality derived from the anticommutativity hypothesis, but compilation fails because commutative-ring tactics do not expand the non-commutative goals.

  • The proposer targets `pow_add_pow_eq`, proving both square identities from `a * b = -(b * a)`.
  • The proof derives `a * b + b * a = 0` and attempts to use it after simplifying both square goals.
  • The first iteration ends with a Lean build failure for the temporary theorem file.
  • Lean reports that `ring_nf` makes no progress and that rewriting fails because `a * b + b * a` is absent from the target.
  • The failure arises because the theorem uses a general, potentially non-commutative `Ring`, whereas `ring` and `ring_nf` assume commutativity.

C.2. Second iteration

The second iteration uses feedback from the failed proof to diagnose the tactic mismatch and proposes manual algebraic expansion with distributivity lemmas, although the supplied attempt still fails to compile.

  • The agent receives the previous failed attempt and its lessons as context for another proof iteration.
  • The recorded proof attempt still fails because `ring_nf` makes no progress and the rewrite cannot find the cross-term pattern.
  • The revised diagnosis identifies that non-commutative goals require manual expansion rather than `ring` or `ring_nf` normalization.
  • The proposed expansion rewrites `(a + b)^2` into `a*a + a*b + b*a + b*b`, then cancels the cross terms using `a * b + b * a = 0`.
  • The subtraction case analogously uses `sub_mul` and `mul_sub` to obtain `a^2 - (a * b + b * a) + b^2`.
  • The proof structure is judged logically sound in its helper lemmas and algebraic plan, despite the tactic-level compilation failure.

D. Ablation dataset

The ablation studies use a dataset of 100 randomly selected Putnam competition problems.

  • 100 problems were randomly extracted from the Putnam competition for the ablation studies.

E. Error analysis

The error analysis classifies failed proof attempts by their first build error, using six categories that distinguish early code failures from later proof failures.

  • Each failed proof attempt is assigned its first error category, reducing complications from subsequent related errors.
  • The six categories are bad import, name error, sorry remains, syntax error, tactic failure, and unsolved goals.
  • Lower-level errors can prevent Lean from reaching proof checking, while tactic failures and unsolved goals usually occur after parsing and elaboration succeed.

E.1. Ablation comparison

The ablations show that memory and search improve proof success by reducing low-level errors, shifting failures toward higher-level unsolved goals. Stronger foundation models exhibit the same shift, with substantially fewer import, naming, and syntax errors.

  • Agent ablations: Search tools improve success beyond feedback and memory, but less than the preceding improvements.The full system combines self-reflection with search tools, while library search is described as helpful but comparatively less impactful.
  • Error distribution: 13% to 7%: name-error frequency falls as the full system replaces low-level failures with more unsolved-goal errors.Unsolved goals rise from 27% to 36%, while total higher-level errors remain approximately stable, indicating a shift in error composition.
  • Agent ablations: Memory mechanisms significantly reduce errors and provide the second-largest performance boost.Both recent-attempt history and self-managed context let the agent spend more iterations addressing open goals.
  • Memory mechanisms: Self-managed context reduces syntax errors and tactic misuses more than recent-attempt history, producing a larger fraction of unsolved goals.The effect becomes more pronounced when search tools are added to self-managed context.
  • Foundation models: 56% and 33% of failed Gemini Flash and Pro attempts contain bad imports, versus 1% and 0.4% for Claude Sonnet and Opus.These percentages are directly comparable because they concern the first error in each failed proof attempt, and imports occur at the file top.
  • Foundation models: Frontier models shift errors from trivial to deeper categories by making fewer import, naming, and syntax errors while retaining similar tactic failures and unsolved goals.The paper links this shift, together with architectural improvements, to greater benefit from the agentic framework.

F. Cost-performance analysis

The cost analysis measures success against token budgets and separates input from output tokens. AxProverBase reaches competitive success rates with substantially lower token budgets than the compared Hilbert system on PutnamBench.

  • Cost methodology: Success rate is evaluated against maximum and average tokens per problem, with input and output tokens reported separately because their costs differ.The analysis uses Pareto frontiers to compare performance-cost trade-offs across datasets and methods.
  • PutnamBench: 54.7% success on PutnamBench requires 4.2M maximum tokens per problem and 1.4M average tokens, with 2.4 times more input than output tokens.The average output fraction is 29.7% with a 6.2 standard deviation.
  • PutnamBench: 55.9% pass@1 for Hilbert uses a maximum of 1880.4M tokens per problem, while AxProverBase reaches comparable peak performance at about two orders of magnitude fewer tokens.The Pareto frontier indicates better scaling for AxProverBase.
  • LeanCat: 59.0% success on LeanCat is achieved with 1.9M maximum tokens and 0.6M average tokens per problem.Output tokens account for 26.2% of total tokens on average, with an 8.1 standard deviation.

F.3. FATE

The FATE analysis reports performance and token usage separately for the M, H, and X splits. AxProverBase is compared with specialized and general-purpose theorem provers under matched computational considerations.

  • FATE splits: 98.0%, 66.0%, and 24.0% success rates are reported for FATE-M, FATE-H, and FATE-X, respectively.The corresponding maximum token budgets are 1.4M, 2.8M, and 2.9M tokens per problem.
  • FATE splits: FATE Figure 8 places the M, H, and X splits in columns and shows average-token pass rates, maximum-token Pareto frontiers, and input-output token distributions from top to bottom.This layout supports separate cost-performance comparisons for each split.
  • Compared methods: Specialized DeepSeek, Goedel, and Kimina provers outperform general-purpose Qwen3 and DeepSeek-R1 on the compared FATE evaluation.Qwen3 and DeepSeek-R1 cannot prove any problem in the FATE-H dataset.
  • Compared methods: 4x: DeepSeek-Prover-V2 achieves four times R1's success rate with the same model size and a similar number of tokens per problem.The comparison is presented as an illustrative case among the evaluated methods.
Loading 2602.24273v3…