AxProver

Name: AxProver
Author: Axiomatic-AI

远程服务

github.com/Axiomatic-AI科研与教育034 周前更新

关于 AxProver

AxProver 是面向 Lean 4 用户的 MCP 服务，可使用 Mathlib 编译代码或自动证明定理。提交任务后异步处理，并可轮询任务状态。

AxProver 通过可流式 HTTP 连接 MCP 客户端，并使用 GitHub OAuth 2.1。它提供代码构建、定理证明和查询任务状态的工具。

远程服务无需本地安装。选择你使用的客户端，复制配置或使用一键安装。

服务地址https://prover.axiomatic-ai.com/mcp/

一键复制安装命令

Claude CodeTerminalclaude mcp add --transport http ax-prover-base https://prover.axiomatic-ai.com/mcp/

Cursor.cursor/mcp.json{"mcpServers":{"ax-prover-base":{"type":"http","url":"https://prover.axiomatic-ai.com/mcp/"}}}在 Cursor 中打开

VS Code.vscode/mcp.json{"servers":{"ax-prover-base":{"type":"http","url":"https://prover.axiomatic-ai.com/mcp/"}}}在 VS Code 中打开

Claude Desktopclaude_desktop_config.json{"mcpServers":{"ax-prover-base":{"type":"http","url":"https://prover.axiomatic-ai.com/mcp/"}}}

Windsurf~/.codeium/windsurf/mcp_config.json{"mcpServers":{"ax-prover-base":{"serverUrl":"https://prover.axiomatic-ai.com/mcp/"}}}

命令在终端中运行；JSON 粘贴到对应客户端的 MCP 配置后重启。需要授权的服务会在首次连接时提示登录。

Lean 4 MCP 服务：使用 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 客户端会自动处理整个流程。

工具	描述
`lean4_build`	在启用了 Mathlib 的沙箱中编译 Lean 4 源代码。代码会发送到外部云服务进行编译；如果需要证明，也会发送代码进行 AI 处理。
`lean4_prove_theorems`	自动证明包含 `sorry` 的 Lean 4 定理。代码会发送到外部云服务进行编译和 AI 证明。