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.
claude mcp add --transport http com.axiomatic-ai-prover https://prover.axiomatic-ai.com/mcp/