Prover

What prover does

The prover MCP server connects MCP clients to Lean 4 workflows with Mathlib. It supports two submitted operations: compiling Lean source and automatically attempting proofs for Lean theorems that contain sorry. A separate polling tool reports the state and result of submitted jobs.

This fits development tasks where an agent needs to validate formal mathematics, check whether Lean code compiles, or request generated proofs for unfinished theorem statements. The service is accessed remotely rather than run as a local Lean installation, according to the provided connection configuration.

How it works

The prover MCP server uses a streamable HTTP endpoint at https://prover.axiomatic-ai.com/mcp/. An MCP client sends source code to one of the submit tools. Each submit operation runs asynchronously and immediately returns a job_id instead of waiting for compilation or proving to finish.

Use lean4_get_job_status with that identifier to check progress and retrieve the result. Continue polling until the job reaches either completed or failed. Compilation takes place in a Mathlib-enabled sandbox. For proving requests, the code is also sent to external services for AI processing.

Authentication uses OAuth 2.1 through GitHub. The README states that the MCP client handles the authentication flow automatically.

Setup and configuration

Add the remote MCP server to an MCP client configuration. The documented example uses Claude Desktop and assigns the server the name ax-prover:

{
  "mcpServers": {
    "ax-prover": {
      "type": "streamable-http",
      "url": "https://prover.axiomatic-ai.com/mcp/"
    }
  }
}

After connecting, complete the GitHub OAuth flow presented by the client. No required environment variables or local build steps are documented in the supplied material.

Tools and capabilities

• lean4_build compiles Lean 4 source code in a Mathlib-enabled sandbox. The source may be sent to external cloud services for compilation and, where applicable, AI processing.
• lean4_prove_theorems attempts to automatically prove Lean 4 theorems containing sorry. Compilation and AI proving use external cloud services.
• lean4_get_job_status polls an ax-prover job and returns its current status and result.

The first two tools are asynchronous submission operations. Their returned job IDs are required for later polling.

Limitations and notes

The provided material does not describe local execution, configurable compiler versions, supported Mathlib versions, result schemas, timeouts, quotas, or retry behavior. Do not assume that source code stays local: the documented tools send code to external cloud services, and proving requests may involve AI processing. The README specifically demonstrates Claude Desktop; compatibility details for other MCP clients are not documented there.