oOo0oOo/lean-lsp-mcp

lean-lsp-mcp – 用于 Lean 定理证明器的 MCP 服务器

简介 – 这是一个基于 Python 的 Model Context Protocol (MCP) 服务器，运行于 Lean 4 语言服务器之上。它将 Lean 的诊断信息、目标、悬停提示以及一系列搜索工具 (LeanSearch, Loogle, Lean Finder, Lean Hammer) 暴露为 tools，供 LLM 代理程序 (如 Claude Code, Cursor, Mistral Vibe 等) 调用。简而言之，它让 LLM 能像与代码助手对话一样与 Lean 项目交互。

主要功能

• 查询 Lean 诊断信息、当前证明目标、术语定义及悬停文档。
• 执行外部搜索服务 (LeanSearch, Loogle, Lean Finder, Lean Hammer) 以定位相关定理。
• 支持选配的 REPL 驱动 lean_run_code 以进行快速代码执行。
• 可通过环境变量或 MCP 客户端 JSON (VS Code, Cursor, Claude Code, Mistral Vibe) 进行配置。
• 支持三种传输方式：stdio (默认)、streamable-http 以及旧版 sse。
• 支持 OpenAI 的 Secure MCP Tunnel 以实现安全的远程访问。

如何开始使用

1. 安装 uv Python 包管理器 (或使用 Nix)。
2. 确保您的 Lean 项目可以构建 (lake build)。
3. 安装选配工具 – 用于本地搜索的 ripgrep、用于快速代码执行的 repl 包，以及选配的本地 Loogle 二进制文件。
4. 在您的 MCP 兼容 IDE (VS Code, Cursor, Claude Code, Mistral Vibe) 中添加服务器条目 – 大多数示例只需一行指令即可运行 uvx lean-lsp-mcp。
5. (选配) 设置环境变量以调整日志记录、禁用特定工具、调整超时设置或启用验证。

典型工作流程

• LLM 发送请求，例如 “MyProof.lean 中的当前目标是什么？”。
• MCP 服务器调用 Lean LSP，提取目标状态，并返回简洁的文本块。
• 若缺少引理，LLM 可调用 lean_loogle 或 lean_search，查询远程或本地索引并返回匹配的定理。
• 若 LLM 想要尝试证明步骤，它可以调用 lean_run_code (REPL 模式) 或 lean_multi_attempt 来测试代码片段。

安全性注意事项

• 该服务器可以读取项目内的任何文件、执行构建并连接网络以使用搜索工具，因此应在受信任的环境中运行或进行容器化 (提供 Docker 镜像)。
• 通过 HTTP 公开时，请设置 LEAN_LSP_MCP_TOKEN 进行 bearer-token 验证，或使用 OpenAI 的 Secure MCP Tunnel。

使用者群体

• 构建代理式定理证明系统的研究人员 (例如 Ax-Prover, Numina-Lean-Agent, MerLean, M2F) 皆引用此工具。
• 本工具曾于 Lean Together 2026 等会议中发表。

更多信息

• PyPI 包: lean-lsp-mcp
• 源代码与文档: https://github.com/oOo0oOo/lean-lsp-mcp
• 完整工具列表请见 docs/tools.md
• 新增工具的说明文档位于 docs/adding-a-tool.md。

授权条款 – MIT (欢迎引用，但不强制)。