lean-lsp

lean-lsp-mcp exposes an MCP server that integrates Lean theorem prover capabilities with language-server-like interactions. It leverages Lean's language-server-based tooling through leanclient to provide tools such as diagnostics, goal states, term information, hover docs, and a suite of external search aids (LeanSearch, Loogle, Lean Finder, Lean Hammer, Lean State Search). This enables agents and IDEs to query Lean projects, inspect file structure, examine goals and terms, and perform targeted searches across the codebase. Typical workflows include requesting file outlines, retrieving diagnostics for a file, inspecting current goals, and querying symbol information or hover documentation to guide reasoning tasks. The server is designed to work with common MCP clients (e.g., VSCode, Cursor, Claude Code) by exposing a standard set of file interactions and LSP-style capabilities through the MCP protocol.

To use it, run the MCP server in your project workspace and connect your MCP client to the lean-lsp server (named lean-lsp in the MCP config). The recommended startup flow is to first ensure your Lean project builds locally (lake build) to speed up the language server, then start the MCP server using the uvx command with the lean-lsp-mcp package, and finally configure your client to point to the lean-lsp server entry (e.g., via mcp.json or built-in setup wizards). Once connected, you can invoke tools like lean_file_outline, lean_diagnostic_messages, lean_goal, lean_term_goal, lean_hover_info, lean_declaration_file, lean_completions, and lean_run_code to interact with Lean code in an agent-friendly manner.

Prerequisites:

• Python installed (recommended via your system package manager or Anaconda).
• uv (Python package manager) installed. Installation: curl -LsSf https://astral.sh/uv/install.sh | sh
• Lake project should be available in your Lean workspace.
• Optional: ripgrep (rg) for lean_local_search capabilities.

Step-by-step:

1. Install uv as described in the project documentation: curl -LsSf https://astral.sh/uv/install.sh | sh

2. Ensure your Lean project builds locally with lake build (in your project root):

   lake build

3. Install the lean-lsp-mcp package (via pip or your preferred Python tooling as required by your environment).

4. Run the MCP server to start lean-lsp-mcp using uvx (the standard setup shown in the repository examples):

   uvx lean-lsp-mcp

5. Configure your MCP client to connect to the lean-lsp server. For example, in VSCode or Cursor setups, use the provided JSON configurations from the README, typically pointing the server to command "uvx" with argument "lean-lsp-mcp".

6. If you are using Windows with WSL2, you may need to wrap the invocation with wsl.exe and pass uvx lean-lsp-mcp accordingly, as shown in the repository setup examples.

Notes:

• You can also integrate Lean 4 skills or additional search tools to enhance agent interactions.
• Ensure Lean project dependencies are installed and lake build runs cleanly before starting the MCP server for best performance.

Tips and common issues:

• If the MCP client times out during startup, run lake build manually before starting lean-lsp-mcp to speed up initialization.
• For VSCode, Cursor, or Claude Code, follow the exact JSON samples in the README to configure mcp.json or the corresponding UI wizard entries.
• Installing ripgrep (rg) enhances lean_local_search tooling for local project searches.
• If you encounter path issues on Windows with WSL2, use the Windows-in-WSL wrapper (WSL2 integration) as shown in the README snippets.
• The server exposes commands like lean_file_outline, lean_diagnostic_messages, lean_goal, lean_term_goal, lean_hover_info, lean_declaration_file, lean_completions, lean_run_code; use these to build robust agent prompts and toolchains for Lean projects.