Prover

axiomatic-ai/ax-prover-base-mcp

Connects Claude to Axiomatic AI's Lean 4 theorem proving infrastructure over streamable HTTP. You get three core operations: lean4_build compiles code in a Mathlib sandbox, lean4_prove_theorems automatically fills in sorry placeholders using AI, and lean4_get_job_status polls for results since compilation and proving run async. Authentication happens through GitHub OAuth that your MCP client handles. Reach for this when you're formalizing mathematics or need to verify proofs without running a local Lean environment. Code gets sent to their cloud for both compilation and AI processing, so it's trading convenience for keeping everything on your machine.

tools

3

transport

HTTP

last updated

Feb 23, 2026

Sponsors

Promote your product hereReach 125k+ visitors monthlyPromote your product hereReach 125k+ visitors monthlyAgent CaffeineSponsoredClose your lid, come back to finished workSnugSponsoredThe clipboard manager for the AI eraPromote your product hereReach 125k+ visitors monthlyWaxSponsoredBlock anything with supervision, without erasing your iPhonePromote your product hereReach 125k+ visitors monthlyknobsSponsoredSee your site on any phone, any day, in any language

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