LeanTool MCP 服务器使用说明

项目简介

LeanTool 是一个旨在帮助大型语言模型 (LLM) 更好地使用 Lean 证明语言的工具集合。其中 'leanmcp.py' 实现了 Model Context Protocol (MCP) 服务器，允许支持 MCP 协议的客户端（如 Claude Code, Cursor）调用 Lean 代码检查工具。通过此服务器，LLM 客户端可以方便地利用 Lean 证明器的能力，提高在 Lean 代码生成和定理证明任务中的准确性和效率。

主要功能点

提供 Lean 代码检查工具: 通过 'check_lean' 工具，LLM 客户端可以发送 Lean 代码到服务器进行编译和验证，并获取 Lean 证明器的输出结果，包括成功、详细输出信息和错误信息。
支持 Model Context Protocol (MCP): 完全遵循标准的 MCP 协议进行通信，可以与任何兼容 MCP 协议的 LLM 客户端无缝集成。
支持多种运行模式: 灵活支持 stdio 和 SSE (Server-Sent Events) 两种传输协议，满足不同应用场景的需求。
易于集成: 安装配置简单，可以快速集成到现有的 LLM 应用工作流中，为 LLM 提供强大的 Lean 代码处理能力。

安装步骤

安装 Lean 证明器: 请参考仓库 README 文件中的指引，安装 Lean 证明器环境及其依赖。
安装 Poetry: 确保您的系统中已安装 Poetry 依赖管理工具。如果未安装，请根据 Poetry 官方文档进行安装。

克隆仓库: 在您的本地环境中克隆 LeanTool 仓库：

git clone https://github.com/GasStationManager/LeanTool
cd LeanTool

安装 Pantograph 库: 按照仓库 README 中的指引，安装 Pantograph 库，此库用于从 Lean 代码的 'sorry' 占位符中提取目标状态。
安装项目依赖: 在 LeanTool 仓库根目录下，使用 Poetry 安装项目依赖：
```
poetry install
```
配置 LLM 模型 (可选): 如果您希望 LeanTool 的完整功能（包括反馈循环）与 LLM 模型结合使用，请根据仓库 README 配置 LiteLLM 以连接到您选择的 LLM 模型 (例如 OpenAI, Anthropic, Ollama 等)。对于仅使用 MCP 服务器功能，此步骤是可选的。

服务器配置

MCP 服务器需要配置在 MCP 客户端中。以下是两种运行模式 (stdio 和 SSE) 的配置示例，您需要根据您的 MCP 客户端的要求选择其中一种配置，并将配置信息填入客户端的 MCP 服务器配置界面。

1. stdio 模式配置 (推荐 Claude Code 等客户端使用):

{
  "serverName": "LeanToolMCP-stdio",  // MCP 服务器名称，可自定义，用于在客户端中标识
  "command": "poetry run python leanmcp.py", // 启动 MCP 服务器的命令，指向 leanmcp.py 脚本
  "args": [], // 启动参数，stdio 模式通常无需额外参数
  "transport": "stdio" // 指定使用 stdio 传输协议
}

2. SSE 模式配置 (推荐 Cursor 等客户端使用):

{
  "serverName": "LeanToolMCP-sse",  // MCP 服务器名称，可自定义，用于在客户端中标识
  "command": "poetry run python leanmcp.py", // 启动 MCP 服务器的命令，指向 leanmcp.py 脚本
  "args": ["--sse", "--port", "8008"], // 启动参数，指定使用 SSE 协议和端口号 8008
  "transport": "sse", // 指定使用 SSE 传输协议
  "baseUrl": "http://<your-host-or-ip-address>:8008/sse" // SSE 服务器 URL，需要将 <your-host-or-ip-address> 替换为运行 MCP 服务器的主机名或 IP 地址
}

配置参数说明:

'serverName': MCP 服务器的名称，您可以自定义设置，用于在 MCP 客户端中识别和管理不同的 MCP 服务器连接。
'command': 启动 MCP 服务器的命令。对于 LeanTool MCP 服务器，此命令通常为 'poetry run python leanmcp.py'，它会使用 Poetry 环境运行 'leanmcp.py' 脚本。
'args': 启动命令的参数。
- 对于 stdio 模式，'args' 通常为空数组 '[]'。
- 对于 SSE 模式，'args' 需要包含 '"--sse"' 以启用 SSE 模式，以及 '"--port"' 和端口号 (例如 '"8008"') 来指定服务器监听的端口。
'transport': 指定 MCP 服务器使用的传输协议。
- '"stdio"': 使用标准输入输出流进行通信，适用于 Claude Code 等客户端。
- '"sse"': 使用 Server-Sent Events 协议进行通信，适用于 Cursor 等客户端。
'baseUrl' (仅 SSE 模式需要): SSE 服务器的 URL。您需要将 '<your-host-or-ip-address>' 替换为实际运行 MCP 服务器的主机名或 IP 地址。端口号需要与 'args' 中指定的端口号一致。

重要提示:

请根据您的 MCP 客户端所支持的传输协议选择合适的配置模式 (stdio 或 SSE)。
在配置 SSE 模式时，请确保将 '<your-host-or-ip-address>' 和端口号替换为实际的服务器地址和端口。
您可以根据需要修改端口号 (例如 '8008')，但要确保 MCP 客户端和服务器端配置的端口号一致。

基本使用方法

启动 MCP 服务器: 根据您选择的配置模式，在 LeanTool 仓库目录下运行相应的命令启动 'leanmcp.py' 服务器。
- stdio 模式: 在终端中执行 'poetry run python leanmcp.py'。
- SSE 模式: 在终端中执行 'poetry run python leanmcp.py --sse --port 8008' (或您配置的端口号)。
- 启动成功后，服务器将在后台运行，等待 MCP 客户端连接。
配置 MCP 客户端: 打开您的 MCP 客户端 (例如 Claude Code, Cursor)，进入 MCP 服务器配置界面，根据您选择的模式 (stdio 或 SSE)，填入上述提供的 JSON 配置信息。确保配置信息准确无误。
在 LLM 客户端中使用 'check_lean' 工具: 在您的 LLM 客户端中，当您需要检查 Lean 代码时，可以指示 LLM 使用 'check_lean' 工具。具体的调用方式取决于您的 MCP 客户端的界面和提示词设计。例如，您可以在提示词中加入类似 "请使用 'check_lean' 工具检查以下 Lean 代码：" 的指令，并将 Lean 代码提供给 LLM。
查看工具执行结果: MCP 客户端会将 LLM 的工具调用请求发送到 LeanTool MCP 服务器。服务器执行 'check_lean' 工具后，会将 Lean 证明器的输出结果返回给客户端。您可以在客户端界面中查看工具执行的详细结果，包括代码检查是否成功、Lean 的输出信息和错误信息等。这些信息可以帮助您和 LLM 更好地理解 Lean 代码的正确性，并进行后续的迭代和改进。

示例测试 (Cursor 客户端)

按照 SSE 模式配置启动 LeanTool MCP 服务器，并配置 Cursor 客户端连接到该服务器。
在 Cursor 中打开一个 Lean 文件或新建一个 Lean 文件。

在聊天框中输入类似以下提示词:

请检查以下 Lean 4 代码的语法：
```lean
theorem hello : True := by trivial

并将代码发送给 'check_lean' 工具进行检查，返回工具的输出结果。

undefined

Cursor 客户端会识别到 'check_lean' 工具调用，并提示您确认运行工具。点击 "Run tool" 按钮确认运行。
Cursor 会将 Lean 代码发送到 LeanTool MCP 服务器进行检查，并将服务器返回的结果显示在聊天界面中。您应该看到 'check_lean' 工具返回的 Lean 证明器的输出，表明代码语法检查是否成功。

通过以上步骤，您就可以成功配置和使用 LeanTool MCP 服务器，为您的 LLM 客户端提供强大的 Lean 代码检查能力。

LeanTool