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.

Setup

Choose your client, copy the config, then fill in any required environment variables.

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"
      ]
    }
  }
}