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サーバーカタログ。当サイトは独立した第三者ディレクトリであり、各MCPサーバーの提供元との提携や推奨関係はありません。
