English Français العربية

com.axiomatic-ai/prover

Official registry Other

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

Source code Documentation

Install

Add this to your client's MCP configuration (Claude Desktop: claude_desktop_config.json; Cursor: .cursor/mcp.json; VS Code and others use the same "mcpServers" shape).

Remote (streamable-http)
Claude Code 
claude mcp add --transport http prover 'https://prover.axiomatic-ai.com/mcp/'
JSON configuration (Claude Desktop, Cursor, VS Code) 
{
    "mcpServers": {
        "prover": {
            "type": "http",
            "url": "https://prover.axiomatic-ai.com/mcp/"
        }
    }
}

Documentation

From the project's README on GitHub, refreshed weekly. Links open on GitHub.

Contents
  1. Axiomatic Prover — MCP Server
  2. Connect
  3. Tools
  4. Links

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.

Frequently asked questions

What is com.axiomatic-ai/prover?

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

How do I install com.axiomatic-ai/prover?

It runs as a remote server. In Claude Code: claude mcp add --transport http prover 'https://prover.axiomatic-ai.com/mcp/'. For other clients, paste the JSON configuration from this page into their MCP settings.

Does com.axiomatic-ai/prover need an API key?

Its registry entry lists no required key or secret. Some features may still need an account with the service it connects to.

Is com.axiomatic-ai/prover open source?

Its code is public on GitHub, but the repository does not declare a standard license.

Who maintains com.axiomatic-ai/prover?

It is published by Axiomatic-AI. AI.tn lists it but does not maintain or endorse it.

From the official MCP Registry. Listing is not an endorsement: review a server's code and permissions before giving it access to your data.