Lean LSP MCP 的 AI 智能体
通过 Lean LSP MCP 服务器，将智能体交互集成到 Lean 定理证明器中。利用无缝 LSP 连接（支持 VSCode、Cursor、Claude Code 等），解锁高级 Lean 诊断、自动证明、代码补全和定理检索等功能。让大模型智能体高效分析和自动化 Lean 数学证明。
自动证明分析与代码洞察
借助 MCP 服务器，丰富 Lean 文件交互体验。可在 IDE 或智能体工作流中即时获取诊断、证明目标、术语信息、悬停文档和代码自动补全。简化 Lean 项目管理，加速证明开发。
- Lean 文件诊断:
- 接收全面的 Lean 文件错误、警告和信息消息，精准调试和完善证明。
- 证明目标提取:
- 在任意位置提取证明目标，实现 Lean 项目的逐步自动化与验证。
- 悬停信息与文档:
- 即时获取术语与符号悬停信息，提高学习和生产效率。
- 代码补全支持:
- 查找可用标识符和自动补全建议，加快 Lean 代码编写。
集成检索与发现工具
结合 leansearch、loogle、lean_hammer、lean_state_search 等工具，实现高级定理与定义发现。支持大模型智能体和用户快速定位相关证明、定义和数学资源，让 Lean 前所未有地易用。
- 定理与定义检索:
- 借助 leansearch 和 loogle 等外部工具高效检索相关定理和定义。
- 自动证明辅助:
- 结合 lean_hammer 与 lean_state_search 实现高级证明策略与前提选取。
- 工具集成便捷:
- 通过环境变量配置外部检索与证明工具，实现无缝访问。
灵活部署与安全连接
在 VSCode、Cursor、Claude Code 或任意 LSP 兼容客户端中，轻松配置并部署 Lean LSP MCP。支持多种传输方式（如 stdio 和 HTTP 流），并可通过 Bearer Token 认证和灵活环境变量实现安全管控。
- 多客户端支持:
- 无缝连接 VSCode、Cursor、Claude Code 及其他 LSP 兼容工具，实现灵活工作流。
- Bearer Token 认证:
- 通过 Bearer Token 安全认证限制 HTTP/SSE 传输的服务器访问。
- 环境变量配置:
- 通过项目路径、检索 URL 及高级设置自定义集成与访问。
MCP 集成
可用的 Lean LSP MCP 集成工具
以下工具可作为 Lean LSP MCP 集成的一部分使用：
- lean_file_contents
获取 Lean 文件内容，可选带有行号标注。
- lean_diagnostic_messages
获取 Lean 文件的全部诊断信息（信息、警告、错误）。
- lean_goal
获取 Lean 文件指定位置的证明目标，理解当前证明状态。
- lean_term_goal
获取 Lean 文件指定位置（行和列）的术语目标。
- lean_hover_info
获取 Lean 文件某一位置符号或术语的悬停信息或文档。
- lean_declaration_file
获取某一符号或术语声明所在文件的内容。
- lean_completions
查找 Lean 文件指定位置的可用代码补全或导入建议。
- lean_run_code
运行或编译独立的 Lean 代码片段或文件，并返回输出或错误信息。
- lean_multi_attempt
尝试多组 Lean 代码片段，并返回每个的目标状态和诊断信息。
用智能体大模型工具助力 Lean 项目
在 IDE 或智能体平台中，实现与 Lean 定理证明的强大自动化交互。轻松诊断、检索和解决证明，快速设置与高级集成，助力科研、教学与 AI 工作流。
什么是 LeanMCP
LeanMCP 是一个专为机器理解进程（MCP）设计的开发者友好、可扩展且可靠的托管平台。它提供轻量级、无服务器的环境，让用户高效托管、部署和交互 MCP。LeanMCP 专门支持通过 LSP 协议与 Lean 定理证明器的智能体交互，使 AI 智能体和用户能够以编程方式分析、理解和操作 Lean 项目。内置 leansearch、loogle、lean_hammer 和 lean_state_search 等高级检索工具，LeanMCP 简化了定理证明和自动推理流程，为从事形式化验证和数学证明的开发者及 AI 研究者提供强大工具。
功能
LeanMCP 能做什么
LeanMCP 让用户可以充分利用与 Lean 定理证明项目交互的一系列强大功能。你可以访问深入的诊断信息、悬停文档和目标状态，并使用外部工具进行定理检索与证明。该平台易于与多种 IDE 集成，对开发者和 AI 智能体均高度优化。
- 丰富 Lean 交互
- 获取 Lean 项目的诊断、目标状态、术语信息与悬停文档。
- 高级定理检索
- 使用 leansearch、loogle、lean_hammer 和 lean_state_search 等工具查找相关定理与定义。
- 智能体自动化
- 让大模型智能体自动分析、理解与交互 Lean 代码。
- 轻松集成
- 支持 VSCode、Cursor、Claude Code 等多种客户端，设置便捷。
- 无服务器托管
- 无需手动运维服务器，即可在可扩展的无服务器环境中部署和管理 MCP。
什么是 LeanMCP
AI 智能体通过 LeanMCP 可编程地访问 Lean 定理证明器的能力，大幅提升形式化验证、定理证明和数学推理的自动化。智能体可借助 LeanMCP 提出证明步骤建议、分析代码，并提供更强大的形式化数学解决方案，推动 AI 驱动的数学与验证领域的研究和发展。