Prover

com.axiomatic-ai由 axiomatic-ai.com 发布官方发布者v0.1.0更新于 Oct 24, 2026

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

已验证Streamable HTTP可网页运行开发者工具AI 与机器学习

概览

AI 生成的概览

远程 Lean 4 服务器，让助手在 Mathlib 环境中编译 Lean 代码并自动证明含 sorry 的定理，以异步任务返回结果。

可以做什么
  • 在启用 Mathlib 的沙箱中编译 Lean 4 源码并返回 job_id
  • 自动证明含 sorry 的 Lean 4 定理
  • 轮询已提交任务的运行状态与结果，直到完成或失败
适用场景
适合希望让助手检查 Lean 4 / Mathlib 代码或尝试补全未完成证明，而不想自行搭建本地 Lean 工具链的场景。
运行要求
通过 streamable HTTP 连接的远程 MCP 端点；使用 OAuth 2.1 经 GitHub 登录，由 MCP 客户端自动处理。无需本地运行时或环境变量。
安装前请注意
提交的 Lean 代码会发送到外部云服务进行编译，证明时还会用于 AI 处理，请勿提交机密代码。证明任务可能消耗付费或限流的服务额度。任务为异步执行，需要轮询获取结果。

安装

在 SourceWeft 中

  1. 打开 控制台中的 Prover，将其添加到工作区。
  2. 连接 所需的 凭据。它们会被私密存储，绝不会在公开页面上展示。
  3. 为需要使用其工具的对话启用该服务。

Web executable，通过 Streamable HTTP。 远程服务在工作区中配置后即可从网页运行时运行。

交给智能体安装

把这段提示词粘贴到 Claude Code、Codex、Cursor 等智能体，或 SourceWeft 对话中。智能体会读取该服务器的安装指南，先向你展示发布者、端点和登录方式，经你同意后再把它添加到你的客户端。密钥不会写进任何命令。

阅读 https://sourceweft.com/mcp/com.axiomatic-ai%2Fprover/install.md，并按其中说明把这个 MCP 服务器接入我的客户端。修改任何配置之前，先告诉我它的发布者、端点和登录方式，等我确认。不要把 API 密钥写进命令或我会提交的文件；问我密钥应从哪里获取。

查看智能体所依据的安装指南

其他 MCP 客户端

把它添加到你客户端的 mcpServers 配置中。 客户端会在首次连接时完成 OAuth 登录。

{
  "mcpServers": {
    "prover": {
      "type": "http",
      "url": "https://prover.axiomatic-ai.com/mcp/"
    }
  }
}

README

Axiomatic Prover — MCP Server

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

Connect

Add to your MCP client (e.g. Claude Desktop claude_desktop_config.json):

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

Authentication uses OAuth 2.1 via GitHub — your MCP client handles the flow automatically.

Tools

Submit (async — returns a job_id)

ToolDescription
lean4_buildCompile Lean 4 source code in a Mathlib-enabled sandbox. Code is sent to external cloud services for compilation; if proving, also for AI processing.
lean4_prove_theoremsAutomatically prove Lean 4 theorems that contain sorry. Code is sent to external cloud services for compilation and AI proving.

Poll

ToolDescription
lean4_get_job_statusPoll for the status and result of any ax-prover job.

All submit tools are asynchronous — they return a job_id immediately. Poll with lean4_get_job_status(job_id) until status is completed or failed.

Links

来源：README.md，提交 5ade6ba

工具

0
该服务器需要登录，因此 SourceWeft 无法在没有账号的情况下读取其工具，也未收录。已连接账号所能看到的内容可能因账号及其权限而异。

版本历史

1
  1. v0.1.0最新Sep 16, 2026

评分

已满足适用检查项的 75%

该评分衡量此收录条目的完整程度，依据注册中心条目、端点与公开来源计算得出。它不是对服务器本身的评价，也不表示服务器安全或当前可用：可连通性是带日期的检查结果，评分也不包含安装量或用户评价。

  • 近 30 天内可连通必需25 分
  • 已声明认证方式必需10 分
  • 已列出工具15 分

    请让服务器在无凭据时响应 tools/list，或发布可在沙箱中无凭据启动的软件包。

  • 描述必需15 分
  • 图标10 分
  • 文档15 分
  • 许可证10 分

    请在仓库或注册中心条目中声明许可证。