Prover MCP server

official from Axiomatic AI Dormant last commit 7 mo

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

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

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

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

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

file .mcp.json (in your project root)version 0.1.0

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

Before you enable it

An MCP server runs with whatever access you give it. Start with a development account rather than production, and check which tools the server exposes before you let an agent call them unattended.

This server has not seen a commit in 7 mo. It may still work, but nobody is currently fixing it — check the alternatives before you build on it.