About AxProver
AxProver is an MCP server for Lean 4 users who compile code or automate theorem proofs with Mathlib. It runs submissions asynchronously and provides job-status polling.
Key features
- 01Compile Lean 4 code in a Mathlib sandbox
- 02Automatically prove theorems containing sorry
- 03Submit asynchronous jobs
- 04Poll job status and results
Use cases
- 01Compile Lean 4 code with Mathlib
- 02Automate proofs for theorems with sorry
- 03Track a submitted proving job
MCP support
AxProver connects to MCP clients over streamable HTTP and uses OAuth 2.1 via GitHub. It exposes tools for building code, proving theorems, and checking job status.
Configuration
Remote servers need no local install. Pick your client, then copy the config or install in one click.
https://prover.axiomatic-ai.com/mcp/claude mcp add --transport http ax-prover-base https://prover.axiomatic-ai.com/mcp/{"mcpServers":{"ax-prover-base":{"type":"http","url":"https://prover.axiomatic-ai.com/mcp/"}}}Open in Cursor{"servers":{"ax-prover-base":{"type":"http","url":"https://prover.axiomatic-ai.com/mcp/"}}}Open in VS Code{"mcpServers":{"ax-prover-base":{"type":"http","url":"https://prover.axiomatic-ai.com/mcp/"}}}{"mcpServers":{"ax-prover-base":{"serverUrl":"https://prover.axiomatic-ai.com/mcp/"}}}Run commands in a terminal; paste JSON into the client’s MCP config and restart. Servers that need sign-in will prompt on first connect.
Tools
Details
From the project READMEAxiomatic Prover — MCP Server
Lean 4 MCP server: compile and prove theorems with Mathlib.
Connect
Add to your MCP client (e.g. Claude Desktop claude_desktop_config.json):
{
"mcpServers": {
"ax-prover": {
"type": "streamable-http",
"url": "https://prover.axiomatic-ai.com/mcp/"
}
}
}
Authentication uses OAuth 2.1 via GitHub — your MCP client handles the flow automatically.
Tools
Submit (async — returns a job_id)
| Tool | Description |
|---|---|
lean4_build | Compile Lean 4 source code in a Mathlib-enabled sandbox. Code is sent to external cloud services for compilation; if proving, also for AI processing. |
lean4_prove_theorems | Automatically prove Lean 4 theorems that contain sorry. Code is sent to external cloud services for compilation and AI proving. |
Poll
| Tool | Description |
|---|---|
lean4_get_job_status | Poll for the status and result of any ax-prover job. |
All submit tools are asynchronous — they return a job_id immediately.
Poll with lean4_get_job_status(job_id) until status is completed or failed.
Links
Comments
New to MCP?
From what the protocol is to installing your first server, these answers cover most first questions.
An open protocol that defines how AI applications connect to external tools and data in a uniform way. Clients talk to the model; MCP servers provide tools, resources and prompt templates. They exchange standard messages, so one server can be reused by many clients.