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 分

    請在儲存庫或註冊中心條目中宣告授權條款。