Ax-Prover A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics

A multi-agent framework utilizing the Model Context Protocol to equip general-purpose LLMs with Lean tools for automated theorem proving.

Read Paper →
Input Formal Statement
Output Formal Proof
Agents Orchestrator Formal Prover
Tools Lean 4 MCP Lean Search File System

They get lean4 formal theorem and output a working proof. They have three agents: Orchestrator, Prover, Verifier. They have a MCP for communicating with lean4 compiler. Verifier just do simple lean compile so can not be called an agent really. It is more of an interface.

Method

Ax-Prover is implemented as a multi-agent architecture comprising three specialized agents: the Orchestrator, the Prover, and the Verifier. The agents interact with the Lean environment using the Model Context Protocol (MCP) to access specific tools.

Specialized Agents

Orchestrator The Orchestrator manages the task flow across agents. It handles task assignment by receiving user input and instructing the Prover. It manages feedback routing by receiving diagnostic outputs from the Verifier and passing structured feedback to the Prover when errors are detected. The Orchestrator decides when to terminate the loop, which occurs when the Verifier certifies a proof as complete and error-free, or when a configured maximum number of attempts is reached.

Prover The Prover transforms unproven Lean theorems into complete proofs through an incremental process. It writes updates to a .lean file at each step. The process involves:

  1. Identifying target theorems by scanning for unfinished proofs marked with the sorry tactic.
  2. Generating a natural language proof sketch.
  3. Formalizing each step of the sketch into a Lean statement starting with have and ending with sorry.
  4. Proposing Lean tactics sequentially to substitute each sorry placeholder.
  5. Using the lean_diagnostic_messages tool to evaluate each generated step.

If errors are detected or a sorry remains, the Prover attempts to correct the reasoning.

Verifier The Verifier evaluates the correctness of the proof generated by the Prover. It uses filesystem tools to access the output file and the lean_diagnostic_messages tool to compile the file and parse diagnostic messages. A proof is verified if no level-1 errors exist and no sorry or admit tactics are present in the file.

MCP Tools

The agents interact with the Lean environment through the Model Context Protocol (MCP) using the lean-lsp-mcp interface. This provides access to two tool categories:

  • Filesystem tools: Operations such as read_file, write_file, and list_directory.
  • Lean tools: Functions to search the local library, query external engines (e.g., Loogle, Leansearch), inspect the proof context, and diagnose errors.

Experiments

Experimental Setup

The system was evaluated on two benchmark groups: New Benchmarks (AbstractAlgebra, QuantumTheorems, and NuminaMath-LEAN) and PutnamBench.

  • AbstractAlgebra (AA): 100 Lean problems extracted from an abstract algebra textbook. Problems focus on structural concepts rather than puzzles, such as proving every element \(x = sr^i\) in the dihedral group \(D_n\) has order \(2\).
  • QuantumTheorems (QT): 134 problems covering core quantum mechanics topics, requiring domain-specific concepts like density matrices and observables.
  • NuminaMath-LEAN: 300 problems sampled from a larger collection of competition-level mathematics problems (e.g., determining integers where \((a^2 + b^2)/(ab + 1) \in \mathbb{Z}\)).
  • PutnamBench: 660 formalized problems from the William Lowell Putnam Mathematical Competition.

Ax-Prover (powered by Claude Sonnet 4 or 4.5) was compared against Claude Sonnet 4 without agentic tool access, DeepSeek-Prover-V2-671B, and Kimina-Prover-72B. The evaluation metric was pass@1. For Ax-Prover, a pass@1 evaluation consists of a single execution sequence where reasoning and tool calls are interleaved, bounded by a maximum of 200 API calls and a 25-minute timeout (400 calls and no timeout for PutnamBench). Final results were computed by compiling the generated files with an external Lean compiler.

Results

New Benchmarks On the NuminaMath-LEAN dataset, Ax-Prover solved 51% of the problems. Claude Sonnet 4 solved 5%, DeepSeek-Prover-V2-671B solved 28%, and Kimina-Prover-72B solved 31%.

On the AbstractAlgebra dataset, Ax-Prover solved 64% of the problems. DeepSeek-Prover-V2-671B solved 24%, Kimina-Prover-72B solved 13%, and Claude Sonnet 4 solved 8%.

On the QuantumTheorems dataset, Ax-Prover solved 96% of the problems (100% of easy and 92% of intermediate problems). DeepSeek-Prover-V2-671B solved 61%, Kimina-Prover-72B solved 57%, and Claude Sonnet 4 solved 40%.

PutnamBench Ax-Prover solved 14% of the PutnamBench problems (92 problems). The average proof length generated by Ax-Prover across solved questions was 182 lines.