prover for Claude Code
com.axiomatic-ai/prover
Lean 4 MCP server: compile, prove theorems, and formalize math with Mathlib.
client:Claude Code
transport:streamable-http
Install prover in Claude Code
run in your project directory
claude mcp add --transport http prover https://prover.axiomatic-ai.com/mcp/Adds it for this project only. Append --scope user to make it available everywhere. Claude Code docs