Lean LSP MCP 服务器

“Lean LSP MCP” 服务器能做什么？

Lean LSP MCP 是一个模型上下文协议（MCP）服务器，通过语言服务器协议（LSP）和 leanclient，将 AI 助手与 Lean 定理证明器项目连接起来。它使代理和大语言模型（LLMs）能够与 Lean 项目交互，访问诊断、目标状态、术语信息、悬停文档等功能。这种集成为 Lean 用户简化了开发流程，提供了丰富的以代理为中心的工具集，包括定理搜索、代码补全和项目构建功能。该服务器旨在通过在自动化和交互式场景中使 Lean 工具链可用，提升开发者、研究者和 AI 代理在 Lean 上的体验。

提示词模板列表

在仓库中未找到有关提示词模板的信息。

资源列表

在仓库中未找到有关已开放 MCP 资源的信息。

工具列表

• Lean 定理搜索：通过整合 leansearch.net 允许代理搜索定理。
• 代码补全：为 Lean 文件提供代码补全建议。
• 项目构建：通过 Lean 构建系统实现项目自动化构建。
• 诊断：可访问 Lean 项目的诊断信息。
• 目标状态 & 术语信息：提供目标状态和术语信息，便于深入分析项目。
• 悬停文档：悬停在 Lean 代码元素上时返回文档说明。

典型使用场景

• Lean 项目诊断：即时获取并展示 Lean 项目的代码正确性与调试信息。
• 目标状态探索：检索并展示当前证明开发的目标状态，便于制定证明策略。
• 定理搜索：从 leansearch.net 检索相关定理，辅助构建证明过程。
• Lean 代码补全：为 Lean 代码提供智能补全与建议，提高开发效率。
• 自动项目构建：在自动化工作流或代理代码审查中，触发并监控 Lean 项目构建。

如何配置

Windsurf

1. 确保已安装 uv。
2. 在项目根目录运行 lake build 构建 Lean 项目。
3. 找到 Windsurf 配置文件。
4. 使用以下 JSON 片段添加 Lean LSP MCP 服务器：

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

5. 保存并重启 Windsurf，确认 MCP 服务器已启动。

Claude

1. 安装 uv 并在 Lean 项目中运行 lake build。
2. 打开 Claude 的配置文件。
3. 插入 MCP 服务器配置：

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. 保存并重启 Claude，确认服务器可用。

Cursor

1. 安装 uv 并运行 lake build。
2. 打开 Cursor 的配置文件。
3. 添加 Lean LSP MCP 服务器：

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. 保存更改并重启 Cursor。

Cline

1. 确保已安装 uv 并运行 lake build。
2. 找到并编辑 Cline 的配置文件。
3. 添加服务器：

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. 保存并重启 Cline。

API 密钥安全

如果你的环境需要 API 密钥，请使用环境变量进行安全存储。例如：

{
  "mcpServers": {
    "lean-lsp-mcp": {
      "command": "lean-lsp-mcp",
      "args": [],
      "env": {
        "API_KEY": "${env:LEAN_LSP_MCP_API_KEY}"
      },
      "inputs": {
        "api_key": "${env:LEAN_LSP_MCP_API_KEY}"
      }
    }
  }
}

如何在 FlowHunt 流程中使用 MCP

在 FlowHunt 中集成 MCP

要将 MCP 服务器集成到 FlowHunt 工作流，请先在流程中添加 MCP 组件，并将其连接到你的 AI 代理：

点击 MCP 组件打开配置面板，在系统 MCP 配置部分，使用如下 JSON 格式填写 MCP 服务器信息：

{
  "lean-lsp-mcp": {
    "transport": "streamable_http",
    "url": "https://yourmcpserver.example/pathtothemcp/url"
  }
}

配置完成后，AI 代理即可作为工具使用本 MCP，访问其全部功能。请记得将 “lean-lsp-mcp” 替换为你的 MCP 服务器实际名称，并将 URL 替换为你自己的 MCP 服务器地址。

概览

根据现有文档与代码，Lean LSP MCP 为 Lean 项目提供了强大的工具支持，但缺乏明确的提示词模板与 MCP 资源定义。未提及采样与 roots 支持。总体而言，该服务器对 Lean 用户实用，但尚未开放全部高级 MCP 功能。

MCP 评分