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
- Add JSON configuration to your IDE/Setup.
- Configure env variable LEAN_PROJECT_PATH.
VSCode Insiders
VSCode Insiders (bleeding edge version of VSCode) has introduced agent mode in February 2025. This feature will eventually be released in the stable version of VSCode.
- 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.
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_proofs_complete: Check if all proofs in a file are complete.
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_project_functional: Check if the Lean project and LSP server are functional and responding properly.
-
lean_lsp_restart: Restart the LSP server and optionally rebuild the Lean project.
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
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Filter files by name, interpreter, ABI, and platform.
If you're not sure about the file name format, learn more about wheel file names.
Copy a direct link to the current filters
File details
Details for the file lean_lsp_mcp-0.1.2.tar.gz.
File metadata
- Download URL: lean_lsp_mcp-0.1.2.tar.gz
- Upload date:
- Size: 10.2 kB
- Tags: Source
- Uploaded using Trusted Publishing? No
- Uploaded via:
uv/0.6.10
File hashes
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 |
806c2a23f49f64a449ce83906dd5fe7d73ece5f6d85a63fbde053963eea4ee3a
|
|
| MD5 |
793e42aa5d4cf638fea19d28725110d0
|
|
| BLAKE2b-256 |
e5fd2b1cfbf18bae3990a51ebc8e3ab1a4829a938adbe0e6abfe880482f890bf
|
File details
Details for the file lean_lsp_mcp-0.1.2-py3-none-any.whl.
File metadata
- Download URL: lean_lsp_mcp-0.1.2-py3-none-any.whl
- Upload date:
- Size: 9.2 kB
- Tags: Python 3
- Uploaded using Trusted Publishing? No
- Uploaded via:
uv/0.6.10
File hashes
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 |
68baf11e739c98853459ded0387f2a96cdc06619a491701a8e54e14166cf84df
|
|
| MD5 |
a6aa1b4ce67649cbee18ea003893f3c6
|
|
| BLAKE2b-256 |
7405f01fdd508cec13b7348a0c1dcee6eb562e64deb473a39b9536c332e265b8
|
