Research map / Multi-agent systems and games / LLM agents
A Minimal Agent for Automated Theorem Proving
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes AxProverBase, a minimal ReAct-style Lean 4 proving agent with iterative compiler feedback, a self-managed memory, and library/web search tools, and benchmarks it against specialized provers across PutnamBench, FATE, and LeanCat.
Problem
Modern AI theorem provers are complex, expensive, and hard to compare because gains may come from the base LLM rather than architecture; a simple reproducible baseline is needed.
Approach
A minimal agent loop (proposer LLM, Lean compiler plus LLM reviewer, memory module, optional search tools) where the proposer iteratively refines proofs; ablations isolate the contribution of feedback, memory, and tools, and frontier LLM choice and thinking budget.
Key results
- AxProverBase with Claude Opus 4.5 (32k thinking, 50 iterations) reaches 54.7% pass@1 on PutnamBench, near Hilbert's 55.9%, using far fewer tokens (4.2M vs 1880.4M).
- Reports 98.0% on FATE-M, 66.0% on FATE-H, 24.0% on FATE-X, and 59.0% on LeanCat at pass@1.
- Gemini models show 56% and 33% of errors from bad imports (Gemini 3 Flash and Pro) versus 1.1% and 0.4% for Claude Sonnet and Opus 4.5.
Surprising findings
- Iterative refinement, not search tools, is the largest performance driver; search tools add comparatively little.
- Gemini models import outdated or hallucinated Lean/Mathlib modules despite version specification and search access, wasting iteration budget.
Limitations
- Ablations run on a 100-problem PutnamBench subset with a single frontier model, limiting generality.
- Relies on closed frontier LLM APIs, so cost and reproducibility depend on proprietary models.
- Formal statement faithfulness is only checked by an LLM reviewer plus deterministic checks.
Experimental setup
Datasets: PutnamBench FATE-M FATE-H FATE-X LeanCat
Benchmarks: PutnamBench FATE-M FATE-H FATE-X LeanCat
Metrics: pass@1 pass@k cost per problem token usage
Baselines: DeepSeek-Prover-V2 Goedel-Prover-V2 Kimina Prover Seed-Prover 1.5 Hilbert REAL-Prover Ax-Prover Claude Opus 4.5 single-shot
Builds on: ReAct Ax-Prover LeanSearch LeanInteract
Closest papers by meaning
- Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics (ICML 2026 · similarity 0.91)
- ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.90)
- MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.88)
- Magnushammer: A Transformer-Based Approach to Premise Selection (ICLR 2024 · similarity 0.88)
- BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving (AAAI 2024 · similarity 0.88)
- Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers (ICML 2026 · similarity 0.87)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.