lean-lsp-mcp

该 MCP 服务器允许通过 Language Server Protocol 使用 leanclient 与 Lean 定理证明器进行代理交互。提供工具帮助 LLM 代理理解、分析并与 Lean 项目交互。需要一个使用 lake 构建系统的 Lean 项目；在启动 MCP 服务器前，请手动运行 'lake build'。可选地配置 LEAN_PROJECT_PATH 环境变量以指定 Lean 项目路径。