MCP for Copilot DirectoryMethodologySubmit / Get featuredNewsletter

← Directory

prover

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

likely compatible

OAuth with discovery metadata and Dynamic Client Registration; use OAuth 2.0 → Dynamic discovery.

Rule R2c · what this means · Not tested in Copilot Studio.

Registry namecom.axiomatic-ai/prover
Endpoint used for verdicthttps://prover.axiomatic-ai.com/mcp/
Transportsstreamable-http
Auth (Copilot Studio setting)OAuth 2.0 – Dynamic discovery
Last endpoint check2026-10-20T18:10:45Z · HTTP 401
GitHubAxiomatic-AI/ax-prover-base-mcp
Version0.1.0
Registry updated2026-02-23
Track changes like this weekly. New Copilot-ready MCP servers, breakages and auth changes, in one short email.
Is this wrong or out of date? Email us. Data built 2026-10-20.