5 v0.2.6 更新于 2026-11-09

LeanWarp MCP Server

Check and verify Lean 4 proofs on hosted, warm Lean and Mathlib workers.

适用客户端

本地客户端

Claude Desktop、Claude Code、Cursor、Cline 等支持本地 MCP 的客户端

本地运行(pypi)

{
  "mcpServers": {
    "leanwarp": {
      "command": "uvx",
      "args": [
        "leanwarp"
      ]
    }
  }
}

将上方 JSON 加入 MCP 客户端配置(如 Claude Desktop 的 claude_desktop_config.json 或项目的 .mcp.json)即可接入;远程接入按客户端要求填写 URL 与鉴权头。

check

检查 Lean 文件的错误和警告,--draft 可复用未修改部分的分析结果。

inspect

查看证明中某个位置的目标和局部上下文。

try-tactics

对同一捕获的目标尝试多个 tactic,报告哪些能关闭目标,不修改文件。

verify

由 Lean 内核验证某个声明是否恰好证明了给定的语句。

holes

列出文件中所有 sorry 和 ?_ 洞的位置及前 16 个的目标。

suggest

建议一个能关闭洞的 tactic,仅当证明无其他变化且不引入未证引理或额外公理时才接受。

apply

将 suggest 或 sorry2lemma 的结果写入文件。

sorry2lemma

将仍含 sorry 的定理的证明移入新的命名引理,定理改用该引理。

declarations

列出文件新增的声明及其类型和依赖。

check-files

一次操作中最多检查 64 个文件。

verify-batch

一次操作中最多验证 64 个内联证明,每个结果保留其 custom_id。

connect

为项目创建工作区并自动匹配环境。

wait

等待仍在运行的操作完成。

stop

使用完毕后停止工作区。