AxProver

What is AxProver?

AxProver is an MCP server for Lean 4 that compiles source code and automatically proves theorems using Mathlib. It is designed for developers and mathematicians working with Lean 4 who want to offload theorem proving and compilation to cloud services.

How to use AxProver?

Add the server to your MCP client configuration (e.g., claude_desktop_config.json) with the type streamable-http and URL https://prover.axiomatic-ai.com/mcp/. Authentication uses OAuth 2.1 via GitHub, handled automatically by the client. Submit jobs with lean4_build or lean4_prove_theorems, then poll for results using lean4_get_job_status.

Key features of AxProver

• Compile Lean 4 code in a Mathlib-enabled sandbox.
• Automatically prove theorems containing sorry.
• Asynchronous job execution with immediate job_id return.
• Poll job status until completion or failure.
• OAuth 2.1 authentication via GitHub.

Use cases of AxProver

• Compiling Lean 4 projects without local environment setup.
• Proving unfinished Lean 4 theorems with AI assistance.
• Integrating automated theorem proving into MCP-compatible clients.
• Rapidly testing Lean 4 code snippets against Mathlib.

FAQ from AxProver

What does AxProver do?

AxProver lets you compile Lean 4 code and automatically prove theorems using Mathlib, all through an MCP server. Code is sent to external cloud services for compilation and AI processing.

How is authentication handled?

The server uses OAuth 2.1 via GitHub. Your MCP client automatically manages the authentication flow.

What tools are available?

Three tools: lean4_build (compile), lean4_prove_theorems (prove theorems with sorry), and lean4_get_job_status (poll for results). Submit tools are asynchronous and return a job_id.

Are jobs synchronous or asynchronous?

All submit tools are asynchronous. They return a job_id immediately; use lean4_get_job_status(job_id) to poll until status is completed or failed.

Where does my code execute?

Code is sent to external cloud services for compilation and, if proving, also for AI processing.