Skip to content
mcp/harbor
Verified official

prover MCP

v0.1.0

com.axiomatic-ai/prover

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

transport:streamable-http
View source

Target client

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

This listing does not declare its tools. Connect the server and your client will discover them on the handshake.