← Discover MCPs and Agents
c
MCPAI & MLMCP Registry

com.axiomatic-ai/prover

Lean 4 MCP server: compile, prove theorems, and formalize math with Mathlib.

Links

Repository

README

From the repo.

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)

ToolDescription
lean4_buildCompile 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_theoremsAutomatically prove Lean 4 theorems that contain sorry. Code is sent to external cloud services for compilation and AI proving.

Poll

ToolDescription
lean4_get_job_statusPoll 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

Config for your environment

Use the endpoint URL below in your config. No API key — you connect directly.

Tool

OS

Config file: ~/.cursor/mcp.json

{
  "mcpServers": {
    "mcp-server": {
      "url": "https://prover.axiomatic-ai.com/mcp/"
    }
  }
}

Paste into mcpServers in the config file. Restart Cursor after saving.

If this MCP is also published on mcpchannel.ai, you can subscribe from Browse and use the gateway config there instead.