Summary
Connects Claude to Axiomatic AI's Lean 4 theorem proving infrastructure over streamable HTTP. You get three core operations: lean4_build compiles code in a Mathlib sandbox, lean4_prove_theorems automatically fills in sorry placeholders using AI, and lean4_get_job_status polls for results since compilation and proving run async. Authentication happens through GitHub OAuth that your MCP client handles. Reach for this when you're formalizing mathematics or need to verify proofs without running a local Lean environment. Code gets sent to their cloud for both compilation and AI processing, so it's trading convenience for keeping everything on your machine.
Keep your Mac awake while Claude Code and 40+ AI agents run. Sleeps when they're idle.
One time payment $9 →
Integrate web data into your AI product. One API to scrape website & brand data.
Get API Key Now →
Agent, run crypto. Access onchain data & trade routes via 1inch.
Install now →
On Capafy, your Skill runs online 24/7 as an agent product, and you get paid every time someone uses it.
Start earning →
Axiomatic 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
Featured
Keep your Mac awake while Claude Code and 40+ AI agents run. Sleeps when they're idle.
One time payment $9 →Integrate web data into your AI product. One API to scrape website & brand data.
Get API Key Now →Agent, run crypto. Access onchain data & trade routes via 1inch.
Install now →On Capafy, your Skill runs online 24/7 as an agent product, and you get paid every time someone uses it.
Start earning →