lean-lsp-mcp

Lean Theorem Prover MCP

MCP that allows agentic interaction with the Lean theorem prover via the Language Server Protocol using leanclient. This server provides a range of tools for AI models to understand, analyze and interact with Lean projects.

Currently beta testing: Please help us by submitting bug reports, feedback and feature requests.

Key Features

Rich Lean Interaction: Access diagnostics, goal states, term information, and hover documentation.
Agent-Focused Toolset: Includes tools for theorem search (leansearch.net), code completion, and project builds.
Easy Setup: Simple configuration for various IDEs, including VSCode and Cursor.

Setup

Overview

Install uv, a Python package manager.
Make sure your Lean project builds quickly by running lake build manually.
Add JSON configuration to your IDE/Setup and configure 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. a) 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_PATH to 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. b) Cursor Setup

Open MCP Settings (File > Preferences > Cursor Settings > MCP)
"+ Add a new global MCP Server" > ("Create File")
Paste the server config into mcp.json file and adjust the LEAN_PROJECT_PATH to 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"
            }
        }
    }
}

Other Setups

Other setups, such as Claude Desktop, Claude Code or OpenAI Agent SDK should work with similar configs.

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_declaration_file

Get the file contents where a symbol or term is declared.

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_build

Rebuild the Lean project and restart the Lean LSP server.

Prompts

lean_auto_proof_instructions

Get detailed instructions on how to use the Lean LSP MCP to automatically prove theorems. See above (Meta tools).

Example Uses

Here are a few example prompts and interactions to try. All examples use VSCode (Agent Mode) and Gemini 2.5 Pro (Preview).

Using auto proof prompt

Open unfinished proof. Run prompt "auto proof" in VSCode (Agent Mode) or Cursor will use the lean_auto_proof_instructions tool to get detailed instructions on how to use the Lean LSP MCP to automatically prove theorems.

VS Code Agent Mode

Analyze a theorem

Open Algebra/Lie/Abelian.lean. Example prompt:

"Analyze commutative_ring_iff_abelian_lie_ring thoroughly using various tools such as goal, term goal, hover info. Explain the key proof steps in english.".

Analyzing a theorem in chat

Design proof approaches

Open an incomplete proof such as putnam 1964 b2. Example prompt:

"First analyze the problem statement by checking the goal, hover info and looking up key declarations. Next use up to three queries to leansearch to design three different approaches to solve this problem. Very concisely present each approach and its key challenge."

Designing proof approaches

Notes on MCP Security

There are many valid security concerns with the Model Context Protocol (MCP) in general!

This MCP is meant as a research tool and is currently in beta. While it does not handle any sensitive data such as passwords or API keys, it still includes various security risks:

Access to your local file system.
No rate limiting on tool calls.
No input or output validation.

Please be aware of these risks. Feel free to audit the code and report security issues!

For more information, you can use Awesome MCP Security as a starting point.

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}
}

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

lean_lsp_mcp-0.1.9.tar.gz (17.5 kB view details)

Uploaded May 27, 2025 Source

Built Distribution

If you're not sure about the file name format, learn more about wheel file names.

The dropdown lists show the available interpreters, ABIs, and platforms. Enable javascript to be able to filter the list of wheel files.

lean_lsp_mcp-0.1.9-py3-none-any.whl (14.5 kB view details)

Uploaded May 27, 2025 Python 3

File details

Details for the file lean_lsp_mcp-0.1.9.tar.gz.

File metadata

Download URL: lean_lsp_mcp-0.1.9.tar.gz
Upload date: May 27, 2025
Size: 17.5 kB
Tags: Source
Uploaded using Trusted Publishing? No
Uploaded via: uv/0.6.10

File hashes

Hashes for lean_lsp_mcp-0.1.9.tar.gz
Algorithm	Hash digest
SHA256	`9083d9342919ef8fb8b0c8d1756b366682cb8c1e2661f74258ddc1a689f59bd3`
MD5	`b49be08ce245ebcaa345839e496407d3`
BLAKE2b-256	`3961564267c4e1a9e2e73c850eeb7d7a09a07c7401930410f156e4631cc75efc`

See more details on using hashes here.

File details

Details for the file lean_lsp_mcp-0.1.9-py3-none-any.whl.

File metadata

Download URL: lean_lsp_mcp-0.1.9-py3-none-any.whl
Upload date: May 27, 2025
Size: 14.5 kB
Tags: Python 3
Uploaded using Trusted Publishing? No
Uploaded via: uv/0.6.10

File hashes

Hashes for lean_lsp_mcp-0.1.9-py3-none-any.whl
Algorithm	Hash digest
SHA256	`bd4bdadf8c9301834ab41a24e4ee655507e318e79b636f2669a8d2ab1f45229b`
MD5	`1622d2501790ec0553c53bb644d8ed35`
BLAKE2b-256	`12547ae8bd553d22e23ea6ce7f1d856278243d77b8aacac0a86d307f6640c581`