Lean LSP MCP 服务器

通过 Lean LSP MCP 连接 AI 代理与 Lean 定理证明器项目，访问诊断、代码补全、定理搜索和项目构建工具。

Lean LSP MCP Server AI Integration

“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

确保已安装 uv 。
在项目根目录运行 lake build 构建 Lean 项目。
找到 Windsurf 配置文件。

使用以下 JSON 片段添加 Lean LSP MCP 服务器：

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

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

Claude

安装 uv 并在 Lean 项目中运行 lake build。
打开 Claude 的配置文件。

插入 MCP 服务器配置：

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

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

Cursor

安装 uv 并运行 lake build。
打开 Cursor 的配置文件。

添加 Lean LSP MCP 服务器：

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

保存更改并重启 Cursor。

Cline

确保已安装 uv 并运行 lake build。
找到并编辑 Cline 的配置文件。

添加服务器：

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

保存并重启 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 服务器地址。

概览

板块	可用性	说明/备注
概览	✅
提示词模板列表	⛔	未找到提示词模板
资源列表	⛔	未列出 MCP 资源
工具列表	✅	见 README 与仓库描述
API 密钥安全	✅	提供了示例
采样支持（评测时不重要）	⛔	未提及