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.
- Make sure your Lean project builds quickly by running
lake buildmanually in a terminal in the project root. - Add JSON configuration to your IDE/Setup.
- Configure env variable LEAN_PROJECT_PATH.
1. Install uv
Install uv for your system.
E.g. on Linux/MacOS:
curl -LsSf https://astral.sh/uv/install.sh | sh
2. Run lake build
lean-lsp-mcp will run lake build in the project root upon startup. Some IDEs (like Cursor) might timeout during this process. Therefore, it is recommended to run lake build manually before starting the MCP. This ensures a faster startup time and avoids timeouts.
E.g. on Linux/MacOS:
cd /path/to/lean/project
lake build
Note: Your build does not necessarily need to be successful, some errors or warnings (e.g. declaration uses 'sorry') are OK.
3. VSCode Setup
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:
3. Cursor Setup
-
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 theorem prover:
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. You can check out the current instruction prompt in prompts.py.
Core interactions
lean_diagnostic_messages
Get all diagnostic messages for a Lean file. This includes infos, warnings and errors.
Example output
l20c42-l20c46, severity: 1
simp made no progress
l21c11-l21c45, severity: 1
function expected at
h_empty
term has type
T ∩ compl T = ∅
...
lean_goal
Get the proof goal at a specific location (line or line & column) in a Lean file.
Example output (line)
Before:S : Type u_1
inst✝¹ : Fintype S
inst✝ : Nonempty S
P : Finset (Set S)
hPP : ∀ T ∈ P, ∀ U ∈ P, T ∩ U ≠ ∅
hPS : ¬∃ T ∉ P, ∀ U ∈ P, T ∩ U ≠ ∅
compl : Set S → Set S := fun T ↦ univ \ T
hcompl : ∀ T ∈ P, compl T ∉ P
all_subsets : Finset (Set S) := Finset.univ
h_comp_in_P : ∀ T ∉ P, compl T ∈ P
h_partition : ∀ (T : Set S), T ∈ P ∨ compl T ∈ P
⊢ P.card = 2 ^ (Fintype.card S - 1)
After:
no goals
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 `sorry`)
The `sorry` tactic is a temporary placeholder for an incomplete tactic proof,closing the main goal using `exact sorry`.
This is intended for stubbing-out incomplete parts of a proof while still having a syntactically correct proof skeleton.
Lean will give a warning whenever a proof uses sorry, so you aren't likely to miss it,
but you can double check if a theorem depends on sorry by looking for sorryAx in the output
of the #print axioms my_thm command, the axiom used by the implementation of sorry.
lean_completions
Code auto-completion: Find available identifiers or import suggestions at a specific position (line & column) in a Lean file.
lean_leansearch
Search for theorems in Mathlib using leansearch.net (natural language search).
Example output (query by LLM: "finite set, subset, complement, cardinality, half, partition")
{"module_name": ["Mathlib", "Data", "Fintype", "Card"], "kind": "theorem", "name": ["Finset", "card_compl"], "signature": " [DecidableEq \u03b1] [Fintype \u03b1] (s : Finset \u03b1) : #s\u1d9c = Fintype.card \u03b1 - #s", "type": "\u2200 {\u03b1 : Type u_1} [inst : DecidableEq \u03b1] [inst_1 : Fintype \u03b1] (s : Finset \u03b1), s\u1d9c.card = Fintype.card \u03b1 - s.card", "value": ":=\n Finset.card_univ_diff s", "docstring": null, "informal_name": "Cardinality of Complement Set in Finite Type", "informal_description": "For a finite type $\\alpha$ with decidable equality and a finite subset $s \\subseteq \\alpha$, the cardinality of the complement of $s$ equals the difference between the cardinality of $\\alpha$ and the cardinality of $s$, i.e.,\n$$|s^c| = \\text{card}(\\alpha) - |s|.$$"}
...
More answers like above
...
lean_proofs_complete
Check if all proofs in a file are complete. This is currently very simple and will be improved in the future.
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. See above (Meta tools).
Related Projects
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.8
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.8.tar.gz | 14.9 kB | Details |
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Reset |
|---|---|---|---|---|
| lean_lsp_mcp-0.1.8-py3-none-any.whl | Python 3 | none | any | Details |
Total release size: 27.6 kB
Release files / lean_lsp_mcp-0.1.8.tar.gz
| Download URL | lean_lsp_mcp-0.1.8.tar.gz |
|---|---|
| Size | 14.9 kB |
| Tags | Source |
|
SHA-256 checksum How to use checksums |
99e001019c46297037dbea8f9bc1fef02af2fbbf700890dde89960804605f048
|
|
BLAKE2b-256 checksum How to use checksums |
7a555c88e604a0b6a0b9a1014a60d7e95a5e7e42ac4e398844f61d6eb9d5f1d8
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
uv/0.6.10
|
Release files / lean_lsp_mcp-0.1.8-py3-none-any.whl
| Download URL | lean_lsp_mcp-0.1.8-py3-none-any.whl |
|---|---|
| Size | 12.7 kB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
6282cf8951c5de6e4c7962657307638b4206ca1d80c5f429a49ff3a2b7122197
|
|
BLAKE2b-256 checksum How to use checksums |
2411b00f3c1488280e198b23518edd46d997292eba8f834fcfb6d23ceb639b17
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
uv/0.6.10
|
