公理证明器——MCP服务器
精益4MCP服务器：使用Mathlib编译和证明定理。
连接
添加到您的MCP客户端（例如Claude Desktop claude_desktop_config.json):
{
"mcpServers": {
"ax-prover": {
"type": "streamable-http",
"url": "https://prover.axiomatic-ai.com/mcp/"
}
}
}身份验证通过GitHub使用OAuth 2.1——您的MCP客户端会自动处理流程。
工具
Submit（async--返回一个 job_id)
| 工具 | 说明 |
|---|---|
lean4_build | 在支持Mathlib的沙箱中编译精益4源代码。代码被发送到外部云服务进行编译；如果证明，也用于人工智能处理。 |
lean4_prove_theorems | 自动证明包含以下内容的精益4定理 sorry代码被发送到外部云服务进行编译和AI证明。 |
投票
| 工具 | 说明 |
|---|---|
lean4_get_job_status | 轮询任何验斧工的状态和结果。 |
所有提交工具都是异步的——它们返回一个 job_id 立即。 投票与 lean4_get_job_status(job_id) 直到状态为 completed 或 failed.