prover — Claude Code MCP server for Lean 4 proofs
Compile Lean 4 code with Mathlib and ask the server to attempt proofs for unfinished theorems. Connect it when you want an agent to run these jobs and check their results.
claude mcp add --transport http prover https://prover.axiomatic-ai.com/mcp/What prover does
prover exposes tools for compiling Lean 4 code in a Mathlib-enabled environment. lean4_build runs a compilation job; lean4_prove_theorems tries to fill in theorems marked with sorry. Jobs run asynchronously. Each submission returns a job_id, which you can pass to lean4_get_job_status to retrieve its state and result.
Access uses OAuth 2.1 through GitHub, with the MCP client handling authorization. Source code goes to external cloud services for compilation, and theorem-proving jobs also send it for AI processing. That matters if your code contains material that must stay within your own environment. The server supports Claude Code and the other platforms listed for this entry.
What it helps with
- compile Lean 4 source with Mathlib
- attempt proofs for theorems marked
sorry - check the progress of a submitted job
- retrieve a compilation or proof result
Example prompts for the agent
- Compile this Lean 4 code using
lean4_build. - Try to prove the theorems marked
sorrywithlean4_prove_theorems. - Check job
job_idusinglean4_get_job_status.
How to install prover
Platform CLI: remote server
claude mcp add --transport http prover https://prover.axiomatic-ai.com/mcp/Platform CLI: remote server
codex mcp add prover --url https://prover.axiomatic-ai.com/mcp/Config file
{
"mcpServers": {
"prover": {
"url": "https://prover.axiomatic-ai.com/mcp/"
}
}
}Config file
{
"servers": {
"prover": {
"type": "http",
"url": "https://prover.axiomatic-ai.com/mcp/"
}
}
}Platform CLI: remote server
gemini mcp add -t http prover https://prover.axiomatic-ai.com/mcp/Step by step, with commands for each platform: How to add an MCP server to Claude Code, Codex, Cursor, VS Code, Gemini CLI and more
Questions about prover
How do I install prover in Claude Code?
Run claude mcp add --transport http prover https://prover.axiomatic-ai.com/mcp/. Authorization uses OAuth 2.1 through GitHub.
What does prover do?
It compiles Lean 4 code with Mathlib and attempts proofs for theorems marked sorry. Jobs run asynchronously, and lean4_get_job_status returns their status and result.
Where does prover process submitted code?
External cloud services receive the code for compilation; theorem-proving jobs also send it for AI processing.
