Axiomatic Prover — MCP Server
MCP serverDev toolsOnce this integration is added, your AI can compile Lean 4 code, prove theorems, and formalize math using the Mathlib library. Lean 4 is a language for writing formal math and proofs, and Mathlib is a math library for Lean.
Use Axiomatic Prover — MCP Server in Claude, ChatGPT or Ahel Desktop
Free. Sign in, add Axiomatic Prover — MCP Server and connect your AI. About a minute.
Also: Claude Code · Cursor · Codex
Then ask your AI: use Axiomatic Prover
Needs your own Axiomatic Prover — MCP Server account. You sign in to it and approve access when you connect.
Details
Available today. Use it from your connected AI after setup.
After adding it, ask your AI to compile some Lean code or prove a theorem to try it out.
What your AI can do with it
- Compile Lean 4 code
- Prove theorems in Lean 4
- Formalize math in Lean 4
- Work with the Mathlib math library
Install Axiomatic Prover — MCP Server
The server’s own address, for the clients that take one directly. Or connect Ahel once and every client you use reads it from one address, with the account kept on Ahel rather than in each client’s config.
Claude Code
claude mcp add --transport http --scope user axiomatic-prover-mcp-server 'https://prover.axiomatic-ai.com/mcp/'Run it once in your project, then open /mcp to approve any sign-in the server asks for.
Claude Desktop
https://prover.axiomatic-ai.com/mcp/Add a custom connector in Settings, paste this address, and approve the sign-in.
Cursor
cursor://anysphere.cursor-deeplink/mcp/install?name=axiomatic-prover-mcp-server&config=eyJ1cmwiOiJodHRwczovL3Byb3Zlci5heGlvbWF0aWMtYWkuY29tL21jcC8ifQ==Open the link and Cursor adds the server at that address.
ChatGPT
https://prover.axiomatic-ai.com/mcp/In Settings, enable Developer mode, create an MCP app, and paste this address. Your plan and workspace must allow custom apps.
Codex
codex mcp add axiomatic-prover-mcp-server --url 'https://prover.axiomatic-ai.com/mcp/'Run it once, then sign in with codex mcp login axiomatic-prover-mcp-server if the server asks for an account.
From the project's README
As published by axiomatic-ai/ax-prover-base-mcp in README.md.
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
Signals
- Last commit
- Mar 2026
Advanced
- Delivery
- prover MCP server → your Ahel connector (mcp.ahel.ai) → your AI.
- Item type
- mcp-server
- Key
com-axiomatic-ai-prover- Source
- github.com/axiomatic-ai/ax-prover-base-mcp
- Hosted endpoint
https://prover.axiomatic-ai.com/mcp/
github.com/axiomatic-ai/ax-prover-base-mcp