Lean LSP MCP

Name: Lean LSP MCP
Author: oOo0oOo

oOo0oOo

Lets agents interact with the Lean theorem prover through the Language Server Protocol, reading goals, diagnostics and definitions.

接入配置

选择客户端，复制配置，再按项目文档补齐环境变量。

claude mcp add lean-lsp -- uvx lean-lsp-mcp

~/.codex/config.toml

[mcp_servers.lean-lsp]
command = "uvx"
args = ["lean-lsp-mcp"]

# codex mcp add lean-lsp -- uvx lean-lsp-mcp

~/.cursor/mcp.json

{
  "mcpServers": {
    "lean-lsp": {
      "command": "uvx",
      "args": [
        "lean-lsp-mcp"
      ]
    }
  }
}

.vscode/mcp.json

{
  "servers": {
    "lean-lsp": {
      "type": "stdio",
      "command": "uvx",
      "args": [
        "lean-lsp-mcp"
      ]
    }
  }
}

~/.gemini/settings.json

{
  "mcpServers": {
    "lean-lsp": {
      "command": "uvx",
      "args": [
        "lean-lsp-mcp"
      ]
    }
  }
}

claude_desktop_config.json

{
  "mcpServers": {
    "lean-lsp": {
      "command": "uvx",
      "args": [
        "lean-lsp-mcp"
      ]
    }
  }
}

.trae/mcp.json

{
  "mcpServers": {
    "lean-lsp": {
      "command": "uvx",
      "args": [
        "lean-lsp-mcp"
      ]
    }
  }
}