MCPHUB LogoMCPHUB
Back to directory
lean-lsp-mcp

lean-lsp-mcp

@oOo0oOo360

MCP server that allows agentic interaction with the Lean theorem prover via the Language Server Protocol using leanclient

leantheorem proverlspmathematicsformal verificationtool

Installation & Configuration

{
  "servers": {
    "lean-lsp": {
      "type": "stdio",
      "command": "uvx",
      "args": [
        "lean-lsp-mcp"
      ],
      "env": {
        "LEAN_PROJECT_PATH": "/path/to/lean/project"
      }
    }
  }
}

Information

Transport
stdiostreamablesse
Language
Python
Created
2025/3/29
Updated
2026/6/7
Homepage
https://github.com/oOo0oOo/lean-lsp-mcp