Prover

com.axiomatic-aiPublished by axiomatic-ai.comOfficial publisherv0.1.0Updated Oct 24, 2026

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

VerifiedStreamable HTTPWeb executableDeveloper ToolsAI & ML

Overview

AI-generated overview

Remote Lean 4 server that lets an assistant compile Lean code with Mathlib and auto-prove theorems containing sorry, returning async job results.

What you can do
  • Compile Lean 4 source in a Mathlib-enabled sandbox and get a job_id back
  • Automatically prove Lean 4 theorems that contain sorry
  • Poll any submitted job for its status and result until it completes or fails
When to use it
Useful when you want an assistant to check Lean 4 / Mathlib code or attempt to fill in unfinished proofs without setting up a local Lean toolchain.
Requirements
A remote MCP endpoint over streamable HTTP; OAuth 2.1 sign-in via GitHub, handled by the MCP client. No local runtime or environment variables are needed.
Before you install
Submitted Lean code is sent to external cloud services for compilation, and for AI processing when proving; avoid sending confidential code. Proving jobs may consume paid or rate-limited service capacity. Jobs are asynchronous, so results must be polled.

Installation

In SourceWeft

  1. Open Prover in the dashboard and add it to a workspace.
  2. Connect the required credentials. They are stored privately and never shown on public pages.
  3. Enable the server for the chats that should use its tools.

Web executable via Streamable HTTP. Remote servers run from the web runtime once configured in a workspace.

Use with an agent

Paste this prompt into Claude Code, Codex, Cursor or another agent — or into SourceWeft chat. The agent reads this server's install guide, shows you its publisher, endpoint and sign-in, and adds it to your client once you agree. Keys never go into a command.

Read https://sourceweft.com/mcp/com.axiomatic-ai%2Fprover/install.md and connect the MCP server it describes to my client. Before changing any config, show me its publisher, endpoint and sign-in method and wait for my OK. Never put an API key in a command or in a file I would commit; ask me where it should come from.

Read the install guide the agent follows

Other MCP clients

Add this to your client's mcpServers config. The client completes OAuth sign-in on first connect.

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

README

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):

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

Source: README.md at commit 5ade6ba

Tools

0
This server asks you to sign in, so SourceWeft could not read its tools without an account and has not indexed them. What a connected account sees can depend on that account and its permissions.

Version history

1
  1. v0.1.0LatestSep 16, 2026

Score

75% of the applicable checks met

How complete this listing is, computed from the registry entry, the endpoint and public sources. Not a rating of the server and not a statement that it is safe or working today: reachability is a dated check, and no installs or reviews go into the score.

  • Reached in the last 30 daysRequired25 pts
  • Auth declaredRequired10 pts
  • Tools listed15 pts

    Answer tools/list without a credential, or ship a package that starts in a sandbox without one.

  • DescriptionRequired15 pts
  • Logo10 pts
  • Documentation15 pts
  • License10 pts

    Declare a license in the repository or the registry entry.