{
  "markdown": "# Axiomatic Prover — MCP Server\n\nLean 4 MCP server: compile and prove theorems with Mathlib.\n\n## Connect\n\nAdd to your MCP client (e.g. Claude Desktop `claude_desktop_config.json`):\n\n```json\n{\n  \"mcpServers\": {\n    \"ax-prover\": {\n      \"type\": \"streamable-http\",\n      \"url\": \"https://prover.axiomatic-ai.com/mcp/\"\n    }\n  }\n}\n```\n\nAuthentication uses OAuth 2.1 via GitHub — your MCP client handles the flow automatically.\n\n## Tools\n\n### Submit (async — returns a `job_id`)\n\n| Tool | Description |\n|------|-------------|\n| **`lean4_build`** | Compile Lean 4 source code in a Mathlib-enabled sandbox. Code is sent to external cloud services for compilation; if proving, also for AI processing. |\n| **`lean4_prove_theorems`** | Automatically prove Lean 4 theorems that contain `sorry`. Code is sent to external cloud services for compilation and AI proving. |\n\n### Poll\n\n| Tool | Description |\n|------|-------------|\n| **`lean4_get_job_status`** | Poll for the status and result of any ax-prover job. |\n\nAll submit tools are asynchronous — they return a `job_id` immediately.\nPoll with `lean4_get_job_status(job_id)` until status is `completed` or `failed`.\n\n## Links\n\n- [axiomatic-ai.com](https://axiomatic-ai.com)\n- [MCP Registry](https://registry.modelcontextprotocol.io/)\n\n",
  "bytes": 1274,
  "sha": "2a93c2e9e3db2ad877b7f52ec650a777d94149859e95a874350f0575440173b0",
  "repo_slug": "axiomatic-ai/ax-prover-base-mcp",
  "fonte": "repo",
  "truncated": false,
  "api": "https://agentalog.com/api/listings/mcp_com_axiomatic_ai_prover_f181567d/readme"
}