Technical Summary: Ax-Prover

Problem Statement

The development of Large Language Models (LLMs) capable of reliable formal reasoning across diverse scientific domains remains a significant challenge. Current approaches face a dichotomy:

1. Specialized Provers: Models like DeepSeek-Prover, Kimina-Prover, and Goedel-Prover are trained specifically on Lean theorem proving. While they achieve state-of-the-art results on mathematical competition benchmarks (e.g., MiniF2F, PutnamBench), they suffer from limited generalizability. They struggle to adapt to domains outside their training data (e.g., quantum physics or abstract algebra) and are brittle to updates in the evolving Mathlib library, often requiring frequent retraining. Furthermore, they lack the ability to use external tools or collaborate interactively with human experts.
2. General-Purpose LLMs: Models like Claude and GPT possess broad knowledge and strong reasoning capabilities but lack native integration with formal proof assistants. They cannot natively interact with the Lean environment, leading to a sharp division where they are accessible but incapable of producing rigorous, machine-checked proofs.

This gap necessitates a system that combines the broad reasoning and tool-use capabilities of general-purpose LLMs with the strict syntactic rigor and verification power of Lean, without requiring domain-specific retraining or heavy infrastructure.

Methodology

The authors introduce Ax-Prover, a multi-agent agentic framework designed to automate theorem proving in Lean. The system leverages the Model Context Protocol (MCP) to equip general-purpose LLMs with a suite of Lean tools, enabling them to interact with the formal environment dynamically.

System Architecture

Ax-Prover employs a three-agent workflow, where each agent is an LLM with specific prompts:

1. Orchestrator: Acts as a scheduler. It receives the unproven theorem, assigns tasks to the Prover, manages feedback routing from the Verifier, and determines when to terminate the refinement loop.
2. Prover: The constructive core. It iteratively transforms unproven theorems into completed proofs. The Prover follows an incremental process:
   • Identifies target theorems (marked with sorry).
   • Generates a natural language proof sketch.
   • Formalizes the sketch into Lean statements (using have and sorry).
   • Proposes tactics to replace sorry.
   • Uses MCP tools to inspect goals, search for lemmas, and diagnose errors before proceeding to the next step.
3. Verifier: A final gatekeeper that independently compiles the generated Lean file using lean diagnostic messages. It reports errors and ensures no sorry or level-1 errors remain before certifying the proof.

Tool Integration

A critical component of Ax-Prover is its access to Lean tools via the lean-lsp-mcp repository. These tools allow the LLM to:

• File Management: Read, write, and edit .lean files.
• Diagnostics: Compile code and retrieve diagnostic messages to identify syntax or type errors.
• Context Inspection: Query the current proof goal (lean goal) and hover information.
• Search: Search the Mathlib library for relevant theorems (lean leansearch) and declarations by type signature (lean loogle).
• Execution: Run code and attempt multiple proof strategies.

This tool-enhanced reasoning allows the Prover to function like a "cautious mathematician," drafting plans, incrementally exploring ideas, and verifying correctness at every step.

Key Contributions

The paper outlines three primary contributions:

1. Ax-Prover Framework: A lightweight, agentic workflow connecting general-purpose LLMs to Lean tools via MCP. It demonstrates performance on par with or superior to both general-purpose LLMs and specialized provers across mathematics and physics, without requiring domain-specific training or fine-tuning.
2. New Benchmarks: The introduction of two new datasets to evaluate formal reasoning in underrepresented domains:
   • AbstractAlgebra: 100 problems from Dummit & Foote's textbook, focusing on graduate-level research concepts (groups, rings, fields) rather than competition-style puzzles.
   • QuantumTheorems: 134 problems covering foundational quantum mechanics (density matrices, observables, entropy bounds), bridging theoretical physics with formal verification.
3. Researcher-Friendly Verification: A demonstration of Ax-Prover as an interactive assistant. Through case studies in classical and quantum cryptography, the system collaborates with domain experts to formalize and verify complex security guarantees, lowering the barrier to entry for researchers without Lean expertise.

Results

The authors evaluated Ax-Prover (powered by Claude Sonnet 4) against specialized provers (DeepSeek-Prover-V2-671B, Kimina-Prover-72B) and general-purpose LLMs (Sonnet) on several benchmarks.

• New Benchmarks (AbstractAlgebra & QuantumTheorems):

  • AbstractAlgebra: Ax-Prover achieved 64% accuracy, significantly outperforming DeepSeek-Prover (24%) and Kimina (13%). The specialized models struggled due to the out-of-distribution nature of the research-level algebraic concepts.
  • QuantumTheorems: Ax-Prover achieved 96% overall accuracy (100% on easy, 92% on intermediate), compared to 61% for DeepSeek-Prover and 57% for Kimina. The specialized models failed to generalize to custom physics definitions (e.g., bra/ket, density matrices) absent from standard Mathlib.
  • NuminaMath-LEAN: Ax-Prover scored 51% overall, outperforming DeepSeek-Prover (28%) and Kimina (31%), while the base LLM (Sonnet) scored only 5%.

• PutnamBench:

  • On this challenging undergraduate competition benchmark, Ax-Prover achieved 14% accuracy, ranking as the top open-source model and third overall. It solved 92 problems, surpassing other open-source models like Goedel-Prover-V2 (13%) and DeepSeek-Prover-V2 (7%).
  • Notably, Ax-Prover achieved this with a significantly lower computational budget (pass@1 with a 25-minute timeout) compared to specialized models that often rely on massive parallel attempts (e.g., pass@1024).

• Tool Usage Analysis:

  • The Prover made an average of ~100 tool calls per run, with high success rates (>99%).
  • Ax-Prover utilized a broader set of tactics (including change, suffices, norm_cast) compared to specialized models, which relied heavily on local rewriting. This suggests that tool integration enhances creative exploration and the ability to manage custom definitions.

• Deployment and Cost:

  • Ax-Prover requires only API access, whereas specialized models demand high-end GPU clusters (e.g., H200/A100) and MLOps expertise.
  • While Ax-Prover's API costs were higher than running specialized models on a single pass@1 attempt, the cost difference narrows significantly when specialized models are run with the high pass@n values required for competitive performance (e.g., DeepSeek-Prover at pass@1024 would cost ~$307k for 1000 datapoints vs. ~$4k for Ax-Prover).

Significance and Claims

The paper claims that Ax-Prover offers a generalizable methodology for formal verification across diverse scientific domains, addressing the limitations of specialized systems that struggle to generalize beyond their training data.

• Generalization: Unlike specialized provers that are brittle to library changes and domain shifts, Ax-Prover's tool-based approach allows it to adapt to new definitions (e.g., in quantum physics) and evolving Mathlib versions without retraining.
• Collaboration: The system bridges the gap between AI and human researchers. By acting as an interactive assistant, it enables domain experts to engage in formal verification without needing deep Lean expertise, as demonstrated in the cryptography case studies where it helped identify subtle gaps in informal arguments.
• Efficiency: The framework achieves competitive or superior performance with a "leaner" compute budget, avoiding the need for expensive, specialized infrastructure.

The authors conclude that Ax-Prover represents a step toward verifiable scientific artificial intelligence, where AI systems can contribute to scientific discovery through formally validated reasoning, supporting both autonomous theorem proving and human-AI collaborative research.