lean-lsp-mcp
installs/mo · pypistarsforks
How to install lean-lsp-mcp?
ooo0ooo/lean-lsp-mcp
$git clone https://github.com/oOo0oOo/lean-lsp-mcpMCP server that allows agentic interaction with the Lean theorem prover via the Language Server Protocol using [leanclient](https://github.com/oOo0oOo/leanclie
README.md
| 1 | <h1 align="center"> |
| 2 | lean-lsp-mcp |
| 3 | </h1> |
| 4 | |
| 5 | <h3 align="center">Lean Theorem Prover MCP</h3> |
| 6 | |
| 7 | <p align="center"> |
| 8 | <a href="https://pypi.org/project/lean-lsp-mcp/"> |
| 9 | <img src="https://img.shields.io/pypi/v/lean-lsp-mcp.svg" alt="PyPI version" /> |
| 10 | </a> |
| 11 | <a href=""> |
| 12 | <img src="https://img.shields.io/github/last-commit/oOo0oOo/lean-lsp-mcp" alt="last update" /> |
| 13 | </a> |
| 14 | <a href="https://github.com/oOo0oOo/lean-lsp-mcp/blob/master/LICENSE"> |
| 15 | <img src="https://img.shields.io/github/license/oOo0oOo/lean-lsp-mcp.svg" alt="license" /> |
| 16 | </a> |
| 17 | </p> |
| 18 | |
| 19 | MCP server that allows agentic interaction with the [Lean theorem prover](https://lean-lang.org/) via the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/) using [leanclient](https://github.com/oOo0oOo/leanclient). This server provides a range of tools for LLM agents to understand, analyze and interact with Lean projects. |
| 20 | |
| 21 | ## Key Features |
| 22 | |
| 23 | * **Rich Lean Interaction**: Access diagnostics, goal states, term information, hover documentation and more. |
| 24 | * **External Search Tools**: Use `LeanSearch`, `Loogle`, `Lean Finder`, `Lean Hammer` and `Lean State Search` to find relevant theorems and definitions. |
| 25 | * **Easy Setup**: Simple configuration for various clients, including VSCode, Cursor and Claude Code. |
| 26 | |
| 27 | ## Setup |
| 28 | |
| 29 | ### Overview |
| 30 | |
| 31 | 1. Install [uv](https://docs.astral.sh/uv/getting-started/installation/), a Python package manager. |
| 32 | 2. Make sure your Lean project builds quickly by running `lake build` manually. |
| 33 | 3. Configure your IDE/Setup |
| 34 | 4. (Optional, highly recommended) Install [ripgrep](https://github.com/BurntSushi/ripgrep?tab=readme-ov-file#installation) (`rg`) for local search and source scanning (`lean_verify` warnings). |
| 35 | |
| 36 | ### 1. Install uv |
| 37 | |
| 38 | [Install uv](https://docs.astral.sh/uv/getting-started/installation/) for your system. On Linux/MacOS: `curl -LsSf https://astral.sh/uv/install.sh | sh` |
| 39 | |
| 40 | ### 1b. Alternative: Install with Nix |
| 41 | |
| 42 | If you use Nix, you can install the package directly from GitHub: |
| 43 | |
| 44 | ```bash |
| 45 | nix profile install github:oOo0oOo/lean-lsp-mcp |
| 46 | ``` |
| 47 | |
| 48 | Or run it without installing: `nix run github:oOo0oOo/lean-lsp-mcp`. |
| 49 | |
| 50 | This provides the MCP server only. You still need a Lean toolchain (`elan`/`lake`) for your project, same as the `uv` setup below. |
| 51 | |
| 52 | ### 2. Run `lake build` |
| 53 | |
| 54 | `lean-lsp-mcp` will run `lake serve` 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 `lake build` manually before starting the MCP. This ensures a faster build time and avoids timeouts. |
| 55 | |
| 56 | ### 3. Configure your IDE/Setup |
| 57 | |
| 58 | <details> |
| 59 | <summary><b>VSCode (Click to expand)</b></summary> |
| 60 | One-click config setup: |
| 61 | |
| 62 | [](https://insiders.vscode.dev/redirect/mcp/install?name=lean-lsp&config=%7B%22command%22%3A%22uvx%22%2C%22args%22%3A%5B%22lean-lsp-mcp%22%5D%7D) |
| 63 | |
| 64 | [](https://insiders.vscode.dev/redirect/mcp/install?name=lean-lsp&config=%7B%22command%22%3A%22uvx%22%2C%22args%22%3A%5B%22lean-lsp-mcp%22%5D%7D&quality=insiders) |
| 65 | |
| 66 | OR using the setup wizard: |
| 67 | |
| 68 | Ctrl+Shift+P > "MCP: Add Server..." > "Command (stdio)" > "uvx lean-lsp-mcp" > "lean-lsp" (or any name you like) > Global or Workspace |
| 69 | |
| 70 | OR manually adding config by opening `mcp.json` with: |
| 71 | |
| 72 | Ctrl+Shift+P > "MCP: Open User Configuration" |
| 73 | |
| 74 | and adding the following |
| 75 | |
| 76 | ```jsonc |
| 77 | { |
| 78 | "servers": { |
| 79 | "lean-lsp": { |
| 80 | "type": "stdio", |
| 81 | "command": "uvx", |
| 82 | "args": [ |
| 83 | "lean-lsp-mcp" |
| 84 | ] |
| 85 | } |
| 86 | } |
| 87 | } |
| 88 | ``` |
| 89 | |
| 90 | If you installed VSCode on Windows and are using WSL2 as your development environment, you may need to use this config instead: |
| 91 | |
| 92 | ```jsonc |
| 93 | { |
| 94 | "servers": { |
People who liked this also viewed
6 picksType
- fastapi_mcpExpose your FastAPI endpoints as Model Context Protocol (MCP) tools, with Auth!MCP ServersNov 2025
- rulesyncA Utility CLI for AI Coding AgentsMCP ServersJul 2026
- FunASROpen-source speech recognition toolkit for training, inference, streaming ASR, VAD, punctuation, speaker diarization pipelines, and OpenAI-compatible/MCP serving.MCP ServersJul 2026
- repomix📦 Repomix is a powerful tool that packs your entire repository into a single, AI-friendly file. Perfect for when you need to feed your codebase to Large Language Models (LLMs) or other AI tools like Claude, ChatGPT, DeepSeek, Perplexity, Gemini, Gemma, Llama, Grok, and more.MCP ServersJul 2026
- mcp-serverMCP server for AI-assisted development of CAP applicationsMCP ServersJul 2026
- antigravity-sdk-pythonA Python library for building AI agents that leverage the full power of Google Antigravity.MCP ServersJul 2026
