AI导哈

定理证明服务

Axiomatic Prover是一个基于Lean 4和Mathlib的定理证明服务，提供异步编译和自动证明功能，适用于数学定理的自动化验证。

  • by Axiomatic-AI
  • 云端部署
  • 更新于
在 GitHub 查看 Axiomatic-AI/ax-prover-base-mcp

使用说明

公理证明器——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.

链接

相关 MCP