lean-lsp-mcp
Lean Theorem Prover MCP
MCP that allows agentic interaction with the Lean theorem prover via the Language Server Protocol using leanclient.
Currently beta testing: Please help us by submitting bug reports, feedback and feature requests.
Setup
- Install uv, a Python package manager.
- Add JSON configuration to your IDE/Setup.
- Configure env variable LEAN_PROJECT_PATH.
Install uv
Install uv for your system.
E.g. on Linux/MacOS:
curl -LsSf https://astral.sh/uv/install.sh | sh
VSCode
VSCode and VSCode Insiders are supporting MCPs in agent mode. For VSCode you might have to enable Chat > Agent: Enable in the settings.
- One-click config setup:
OR manually add config to settings.json (global):
{
"mcp": {
"servers": {
"lean-lsp": {
"command": "uvx",
"args": ["lean-lsp-mcp"],
"env": {
"LEAN_PROJECT_PATH": "/path/to/lean/project"
}
}
}
}
}
-
Next change the env variable
LEAN_PROJECT_PATHto point to the root of your Lean project. This is required for the MCP to work. You can also remove this from the config and set this env variable differently. -
Click "Start" above server config, open a Lean file, change to agent mode in the chat and run e.g. "auto proof" to get started:
Cursor
-
Open MCP Settings (File > Preferences > Cursor Settings > MCP)
-
"+ Add a new global MCP Server" > ("Create File")
-
Paste the server config into
mcp.jsonfile and adjust theLEAN_PROJECT_PATHto point to the root of your Lean project:
{
"mcpServers": {
"lean-lsp": {
"command": "uvx",
"args": ["lean-lsp-mcp"],
"env": {
"LEAN_PROJECT_PATH": "/path/to/lean/project"
}
}
}
}
- Open a Lean file and run e.g. "auto proof" in a new chat.
Other Setups
Other setups, such as Claude Desktop, Claude Code or OpenAI Agent SDK should work with similar configs (untested).
Tools
Lean LSP MCP currently provides various tools to interact with the Lean LSP server:
Meta tools
- lean_auto_proof_instructions: Get detailed instructions on how to use the Lean LSP MCP to automatically prove theorems. This is a tool call because many clients do not support prompts yet, it is also available as a prompt.
Core interactions
-
lean_diagnostic_messages: Get all diagnostic messages for a Lean file. This includes infos, warnings and errors.
-
lean_goal: Get the proof goal at a specific location in a Lean file.
-
lean_term_goal: Get the term goal at a specific position.
-
lean_hover_info: Retrieve hover information for symbols, terms, and expressions in a Lean file.
-
lean_completions: Code auto-completion: Find available identifiers or import suggestions.
-
lean_proofs_complete: Check if all proofs in a file are complete.
-
lean_leansearch: Search for theorems in Mathlib using leansearch.net (natural language search).
File operations
- lean_file_contents: Get the contents of a Lean file, optionally with line number annotations.
Project-level tools
-
lean_project_path: Get the path to the current Lean project root directory.
-
lean_lsp_restart: Restart the LSP server and optionally rebuild the Lean project.
Prompts
- lean_auto_proof_instructions: Get detailed instructions on how to use the Lean LSP MCP to automatically prove theorems.
Related Projects
- LeanTool: Provides an MCP "code interpreter" for Lean.
License & Citation
MIT licensed. See LICENSE for more information.
Citing this repository is highly appreciated but not required by the license.
@software{lean-lsp-mcp,
author = {Oliver Dressler},
title = {{Lean LSP MCP: Tools for agentic interaction with the Lean theorem prover}},
url = {https://github.com/oOo0oOo/lean-lsp-mcp},
month = {3},
year = {2025}
}
1 maintainer
Metadata
1 maintainer
Release files for lean-lsp-mcp 0.1.7
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Source distribution (sdist)
| File | Size | Uploaded | |
|---|---|---|---|
| lean_lsp_mcp-0.1.7.tar.gz | 12.1 kB | Details |
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Reset |
|---|---|---|---|---|
| lean_lsp_mcp-0.1.7-py3-none-any.whl | Python 3 | none | any | Details |
Total release size: 23.4 kB
Release files / lean_lsp_mcp-0.1.7.tar.gz
| Download URL | lean_lsp_mcp-0.1.7.tar.gz |
|---|---|
| Size | 12.1 kB |
| Tags | Source |
|
SHA-256 checksum How to use checksums |
eeed402ccb03d8d9298e774db386541066e701f2f53433781a38be3e27867fa3
|
|
BLAKE2b-256 checksum How to use checksums |
e9a23cd2b11526467f16d56598e1e78a877d3ab789fa01ec1e73b381743be729
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
uv/0.6.10
|
Release files / lean_lsp_mcp-0.1.7-py3-none-any.whl
| Download URL | lean_lsp_mcp-0.1.7-py3-none-any.whl |
|---|---|
| Size | 11.3 kB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
e5f20f53287d53962f49d407289bba004e335e6a8df63855e0770e21e3f1aadb
|
|
BLAKE2b-256 checksum How to use checksums |
bf0b0d19afe940e972c5617d71052a1f7b353ece8a08444080bdde290e244567
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
uv/0.6.10
|
