oOo0oOo / lean-lsp-mcp

lean-lsp-mcp Lean Theorem Prover MCP MCP server that allows agentic interaction with the Lean theorem prover via the Language Server Protocol using leanclient. This server provides a range of tools for LLM agents to understand, analyze and interact with Lean projects. Key Features • **Rich Lean Interaction**: Access diagnostics, goal states, term information, hover documentation and more. • **External Search Tools**: Use , , , and to find relevant theorems and definitions. • **Easy Setup**: Simple configuration for various clients, including VSCode, Cursor and Claude Code. Setup Overview • Install uv, a Python package manager. • Make sure your Lean project builds quickly by running manually. • Configure your IDE/Setup • (Optional, highly recommended) Install ripgrep ( ) for local search and source scanning ( warnings). • Install uv Install uv for your system. On Linux/MacOS: • Run will run in the project root to use the language server (for most tools). Some clients (e.g. Cursor) might timeout during this process. Therefore, it is recommended to run manually before starting the MCP. This ensures a faster build time and avoids timeouts. • Configure your IDE/Setup VSCode (Click to expand) One-click config setup: OR using the setup wizard: Ctrl+Shift+P > "MCP: Add Server..." > "Command (stdio)" > "uvx lean-lsp-mcp" > "lean-lsp" (or any name you like) > Global or Workspace OR manually adding config by opening with: Ctrl+Shift+P > "MCP: Open User Configuration" and adding the following If you installed VSCode on Windows and are using WSL2 as your development environment, you may need to use this config instead: If that doesn't work, you can try cloning this repository and replace with . Cursor (Click to expand) • Open MCP Settings (File > Preferences > Cursor Settings > MCP) • "+ Add a new global MCP Server" > ("Create File") • Paste the server config into file: Claude Code (Click to expand) Run one of these commands in the root directory of your Lean project (where is located): You can find more details about MCP server configuration for Claude Code here. • Install ripgrep (optional but recommended) For the local search tool , install ripgrep ( ) and make sure it is available in your PATH. • Install the Lean 4 skill (optional but recommended) With any agentic coding platform such as Claude Code or Codex, you can install the Agentic Coding Skill: Lean 4 Theorem Proving. This skill provides additional prompts and templates for interacting with Lean 4 projects, including guidance on using . MCP Tools File interactions (LSP) lean_file_outline Get a concise outline of a Lean file showing imports and declarations with type signatures (theorems, definitions, classes, structures). lean_diagnostic_messages Get all diagnostic messages for a Lean file. This includes infos, warnings and errors. Use ( , , , ) to filter to a single level. returns verbose nested with embedded widgets. For "Try This" suggestions, prefer . Example output lean_goal Get the proof goal at a specific location (line or line & column) in a Lean file. Example output (line) lean_term_goal Get the term goal at a specific position (line & column) in a Lean file. lean_hover_info Retrieve hover information (documentation) for symbols, terms, and expressions in a Lean file (at a specific line & column). Example output (hover info on a ) lean_declaration_file Get the file contents where a symbol or term is declared. lean_references Find all references to a symbol at a given position (line & column), including its declaration. lean_completions Code auto-completion: Find available identifiers or import suggestions at a specific position (line & column) in a Lean file. lean_run_code Run/compile an independent Lean code snippet/file and return the result or error message. Example output (code snippet: ) lean_multi_attempt Attempt multiple tactics at a proof position and return goal state and diagnostics for each. Useful to screen different proof attempts before committing to one. Accepts: • to target a tactic line • optional to target an exact source position, similar to Execution mode: • When and is omitted, uses the REPL tactic mode for up to 5x faster execution (see Environment Variables). • When is provided, uses the LSP path so the attempt is evaluated at the exact source position. Example output (attempting and ) lean_code_actions Get LSP code actions for a line. Returns resolved edits for "Try This" suggestions ( , , ) and other quick fixes. The agent applies the edits using its own editing tools. Example output (line with simp? ) lean_get_widgets Get panel widgets at a position (proof visualizations, , custom widgets). Returns raw widget data - may be verbose. Example output ( #html widget) lean_get_widget_source Get the JavaScript source code of a widget by its (from or with ). Useful for understanding custom widget rendering logic. Returns full JS module - may be verbose. lean_profile_proof Profile a theorem to identify slow tactics. Runs on an isolated copy of the theorem and returns per-line timing data. Example output (profiling a theorem using simp) lean_verify Check theorem soundness: returns axioms used + optional source pattern scan for , , , etc. Standard axioms are , , - anything else (e.g. ) indicates an unsound proof. Source warnings require ripgrep ( ). Example output (theorem using sorry) Local Search Tools lean_local_search Search for Lean definitions and theorems in the local Lean project and stdlib. This is useful to confirm declarations actually exist and prevent hallucinating APIs. This tool requires ripgrep ( ) to be installed and available in your PATH. External Search Tools Currently most external tools are separately **rate limited to 3 requests per 30 seconds**. Please don't ruin the fun for everyone by overusing these amazing free services! Please cite the original authors of these tools if you use them! lean_leansearch Sear…