Lean LSP MCP
Enables LLM agents to interact with the Lean theorem prover through the Language Server Protocol, providing tools for analyzing Lean projects, accessing diagnostics, goal states, documentation, and searching for theorems using both local and external search services.
代码分析
0 个平台
0 项功能
安装
uvx lean-lsp-mcp
把上面的配置写入 MCP 客户端的配置文件（Claude Desktop 为 claude_desktop_config.json），重启客户端后生效。
{
"mcpServers": {
"lean-lsp-mcp": {
"command": "uvx",
"args": [
"lean-lsp-mcp"
],
"env": {
"LEAN_LOG_LEVEL": "<LEAN_LOG_LEVEL>",
"LEAN_HAMMER_URL": "<LEAN_HAMMER_URL>",
"LEAN_LOOGLE_LOCAL": "<LEAN_LOOGLE_LOCAL>",
"LEAN_PROJECT_PATH": "<LEAN_PROJECT_PATH>",
"LEAN_LSP_MCP_TOKEN": "<LEAN_LSP_MCP_TOKEN>",
"LEAN_LOOGLE_CACHE_DIR": "<LEAN_LOOGLE_CACHE_DIR>",
"LEAN_STATE_SEARCH_URL": "<LEAN_STATE_SEARCH_URL>"
}
}
}
}把上面的配置写入 MCP 客户端的配置文件（Claude Desktop 为 claude_desktop_config.json），重启客户端后生效。
数据来源：公开的 MCP Server 目录。本站为独立第三方目录，与各 MCP Server 维护方均无隶属或背书关系；名称与简介如实标注，介绍文案由本站再加工。
