leanforge-mcp

leanforge-mcp

用于在 Lean 4 中进行 AI 驱动形式化证明搜索的 MCP 服务。提交带有 sorry 的定理，即可获得机器验证的证明。本项目实现了 AlphaProof Nexus 中的 Agent A（DeepMind，2026 年 5 月）。

技术栈： Python 3.12+ · FastMCP 3.4+ · FastAPI · React/Vite · Tailwind · Zustand · Biome · Lean 4 / Mathlib

---

目录

• 功能介绍
• 快速安装
• 你可以做什么
• 工具
• 要求
• 文档
• 状态
• 许可证

---

功能介绍

输入一个带有 sorry 占位符的 Lean 4 定理。系统会循环运行 N 个并行 Agent：大模型提出证明修改，Lean 编译器负责判定，再将错误反馈给大模型。第一个生成不含 sorry 且编译通过的 Agent 即获胜。

-- Input
theorem sum_formula (n : ℕ) : 2 * ∑ i ∈ Finset.range (n + 1), i = n * (n + 1) := by
  sorry

-- Output (machine-verified)
theorem sum_formula (n : ℕ) : 2 * ∑ i ∈ Finset.range (n + 1), i = n * (n + 1) := by
  induction n with
  | zero => simp
  | succ n ih => rw [Finset.sum_range_succ]; ring_nf; linarith

编译器是唯一的判定标准——只要不含 sorry 且编译通过，证明就是正确的。

---

快速安装

git clone https://github.com/sandraschi/leanforge-mcp
cd leanforge-mcp
uv sync
Copy-Item config.example.toml config.toml

然后添加到 claude_desktop_config.json：

{
  "mcpServers": {
    "leanforge": {
      "command": "uv",
      "args": ["--directory", "C:\\path\\to\\leanforge-mcp", "run", "python", "-m", "leanforge_mcp"],
      "env": { "DEEPSEEK_API_KEY": "...", "ANTHROPIC_API_KEY": "..." }
    }
  }
}

Lean + Mathlib 工作区设置请参见 INSTALL.md（约 4 GB，一次性设置；截至 2026-07-09，已在 Goliath 上完成配置并验证）。

---

你可以做什么

"Prove that the sum of the first n natural numbers is n*(n+1)/2"

"Submit this MiniF2F problem and check back in 10 minutes"

"Show me all the proof attempts for job abc-123 -- why is it stuck?"

"Run validate_lean on this tactic proof to see if it compiles"

---

工具

工具	描述
submit_theorem	提交定理陈述 → 作业 ID（异步）
submit_lean_file	提交包含 sorry 占位符的完整 .lean 文件
get_proof_status	轮询作业状态；完成后返回证明
list_attempts	检查每个 Agent/轮次的尝试轨迹
list_jobs	列出所有作业及其状态摘要
validate_lean	直接编译 Lean 4——不跟踪作业
verify_proof	使用已验证的内核（con-leche、con-ron）重新检查已证明的文件——需要 Lean >= 4.35.0 的工作区，参见 docs/VERIFIED_KERNELS.md
cancel_job	取消正在运行的作业
leanforge_shutdown	正常关闭服务（取消正在运行的作业并退出）
get_mathlib_search	使用自然语言搜索 Mathlib 定理

---

要求

• Python 3.11+
• 通过 elan 安装 Lean 4（winget install leanprover.elan）
• 带有缓存 oleans 的 Mathlib 工作区（约 4 GB，一次性设置——参见 INSTALL.md）
• Ollama 和 deepseek-prover-v2:7b，用于 tier-1（本地、免费）
• 用于 tier-2/3 的 DeepSeek 或 Anthropic API 密钥（可选）

---

端口与配置

组件	值
MCP 服务	stdio（uv run python -m leanforge_mcp）
Web 后端（FastAPI）	http://127.0.0.1:10867
Web 前端（Vite）	http://127.0.0.1:10868
配置文件	config.toml（从 config.example.toml 复制；已被 git 忽略）
环境变量	DEEPSEEK_API_KEY（tier 2）、ANTHROPIC_API_KEY（tier 3）——参见 .env.example；密钥保留在服务环境中，不会出现在浏览器中

---

文档

文档	内容
INSTALL.md	前置条件、Lean 工作区设置、Claude Desktop 配置
docs/ONBOARDING.md	新手设置：成本、常见陷阱、健全性检查
docs/CONFIGURATION.md	所有配置选项和环境变量
docs/TOOLS.md	完整的工具参考，含参数和示例
docs/ARCHITECTURE.md	证明循环、层级升级、任务生命周期、SQLite 架构
docs/LEAN.md	Lean 4 语言参考、策略指南、参考书目、链接集
docs/VERIFIED_KERNELS.md	verify_proof 存在的原因、con-leche/con-ron 是什么、工作区升级路径
docs/LEAN_PRIMER.md	面向工程师的 Lean 4 快速入门（简版）
docs/ALPHAPROOF_NEXUS.md	技术介绍：AlphaProof Nexus 论文解析
docs/COVERAGE_GAP.md	为什么 DeepMind 获得了 MSM 覆盖，而初创公司不会
docs/BENCHMARK_RESULTS.md	MiniF2F、PutnamBench、Erdős 结果
docs/DEVELOPMENT.md	贡献、开发环境设置、测试命令
docs/TROUBLESHOOTING.md	常见错误及修复方法
llms-full.txt	完整的 LLM 上下文：工具、端点、配置、端口

---

路线图

阶段	内容	状态
A	核心循环：LLM 提出方案，Lean 进行判断，并反馈错误	已完成
B	强化正确性、处理边界情况、调整超时	已完成（2026-07-09） -- 防篡改保护已修复默认参数截断和诱饵重复项攻击问题，已修复跨进程任务归属和取消问题，并加入无状态提示词缓解措施。真实硬件上的 56/56 项测试均通过。参见 docs/ASSESSMENT_2026-06-24.md
C	性能和安全性：REPL 工作进程池（编译时间才是真正的瓶颈）、LLM 超时/重试、令牌/成本核算（任何批量运行前的硬性门槛）	进行中 -- 参见 TODO.md
D	多 Agent 并行调度（论文中的 Agent B）-- 并行运行 N 个循环，由最先完成者胜出	计划中
E	自我批判步骤 -- LLM 在编译前检查自己的证明，及早发现明显错误	计划中
F	Web 应用证明探索器 -- 以交互式树状视图展示尝试过的证明路径，并实时流式显示策略	计划中
G	前提选择 -- 生成策略前，在 Mathlib 中搜索相关引理	计划中
H	累积式上下文窗口管理 -- 对较长的错误链进行智能摘要，而不是盲目拼接	计划中
I	基准测试仪表板 -- 在 Web 应用页面中按模型/配置跟踪 MiniF2F、PutnamBench、Erdős 结果	延伸计划
J	人在回路 -- Agent 陷入困境时，暂停并展示当前状态，以便人类提供提示	延伸计划
K	证明缓存 -- 对子证明去重，让重复引理能够即时编译	延伸计划

各阶段的作用

A + B 让你可以提交一个定理，并在另一端获得证明。 它能用，也很实用，但它是单线程的，每轮都要完整编译一次，而且没有开销控制——Phase C 弥补了这些不足。

D 改变了局面：N 个并行 Agent 意味着，耗时会从“一个 LLM 要多久”缩短到“N 个 LLM 中最快的一个要多久”。 对于 LLM 会走进死胡同的难题，这意味着耗时从 5 分钟缩短到 30 秒。

E 可防止 LLM 在明显错误的策略上浪费编译时间。 实现成本很低（每次尝试只需额外调用一次 LLM），论文显示，仅在 Agent A 上，它就能将求解率提高约 15 个百分点。

F 是面向用户的价值所在：你不必盯着“status: running”并反复轮询，而是可以实时查看 LLM 尝试各种策略，看到它放弃了哪些路径，并了解它最终成功或失败的原因。

G 针对最常见的失败模式：LLM 为当前上下文中不存在的引理编写了正确的策略。前提选择（生成策略前进行的一项小型检索步骤）能大幅减少这种情况。

H 虽不可见，却至关重要：随着 LLM 累积 10+ 次失败尝试，错误上下文会超出模型的上下文窗口。智能摘要能保留相关信息，同时避免无关内容淹没 LLM。

完整的差距分析：docs/ASSESSMENT_2026-06-24.md

---

许可证

MIT