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.
Code Analysis
0 platforms
0 features
Install
uvx lean-lsp-mcp
Paste the configuration above into your MCP client config (claude_desktop_config.json for Claude Desktop) and restart the client.
{
"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>"
}
}
}
}Paste the configuration above into your MCP client config (claude_desktop_config.json for Claude Desktop) and restart the client.
Sources: public MCP Server directories. This is an independent third-party directory with no affiliation to or endorsement from the maintainers of the listed servers.
