Lean LSP

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

Key Features

• Rich Lean Interaction: Access diagnostics, goal states, term information, hover documentation and more.
• External Search Tools: Use LeanSearch, Loogle, Lean Finder, Lean Hammer and Lean State Search to find relevant theorems and definitions.
• Easy Setup: Simple configuration for various clients, including VSCode, Cursor and Claude Code.

Setup

Overview

1. Install uv, a Python package manager.
2. Make sure your Lean project builds quickly by running lake build manually.
3. Configure your IDE/Setup
4. (Optional, highly recommended) Install ripgrep (rg) for local search and source scanning (lean_verify warnings).

1. Install uv

Install uv for your system. On Linux/MacOS: curl -LsSf https://astral.sh/uv/install.sh | sh

2. Run lake build

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.

3. Configure your IDE/Setup

OR using the setup wizard:

Ctrl+Shift+P > "MCP: Add Server..." > "Command (stdio)" > "uvx lean-lsp-mcp" > "lean-lsp" (or any name you like) > Global or Workspace

OR manually adding config by opening mcp.json with:

Ctrl+Shift+P > "MCP: Open User Configuration"

and adding the following

{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "uvx",
            "args": [
                "lean-lsp-mcp"
            ]
        }
    }
}

If you installed VSCode on Windows and are using WSL2 as your development environment, you may need to use this config instead:

{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "wsl.exe",
            "args": [
                "uvx",
                "lean-lsp-mcp"
            ]
        }
    }
}

If that doesn't work, you can try cloning this repository and replace "lean-lsp-mcp" with "/path/to/cloned/lean-lsp-mcp".

2. "+ Add a new global MCP Server" > ("Create File")

3. Paste the server config into mcp.json file:

{
    "mcpServers": {
        "lean-lsp": {
            "command": "uvx",
            "args": ["lean-lsp-mcp"]
        }
    }
}

# Local-scoped MCP server
claude mcp add lean-lsp uvx lean-lsp-mcp

# OR project-scoped MCP server
# (creates or updates a .mcp.json file in the current directory)
claude mcp add lean-lsp -s project uvx lean-lsp-mcp

You can find more details about MCP server configuration for Claude Code here.

Claude Skill: Lean4 Theorem Proving

If you are using Claude Desktop or Claude Code, you can also install the Lean4 Theorem Proving Skill. This skill provides additional prompts and templates for interacting with Lean4 projects and includes a section on interacting with the lean-lsp-mcp server.

4. Install ripgrep (optional but recommended)

For the local search tool lean_local_search, install ripgrep (rg) and make sure it is available in your PATH.

MCP Tools

File interactions (LSP)

lean_file_outline

Get a concise outline of a Lean file showing imports and declarations with type signatures (theorems, definitions, classes, structures).

lean_diagnostic_messages

Get all diagnostic messages for a Lean file. This includes infos, warnings and errors. interactive=True returns verbose nested TaggedText with embedded widgets. For "Try This" suggestions, prefer lean_code_actions.

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.

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).

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_run_code

Run/compile an independent Lean code snippet/file and return the result or error message.

l1c1-l1c6, severity: 3
38

lean_multi_attempt

Attempt multiple tactics on a line and return goal state and diagnostics for each. Useful to screen different proof attempts before committing to one.

When LEAN_REPL=true, uses the REPL tactic mode for up to 5x faster execution (see Environment Variables).

  rw [Nat.pow_sub (Fintype.card_pos_of_nonempty S)]:
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 ≠ ∅
⊢ P.card = 2 ^ (Fintype.card S - 1)

l14c7-l14c51, severity: 1
unknown constant 'Nat.pow_sub'

  by_contra h_neq:
 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 ≠ ∅
h_neq : ¬P.card = 2 ^ (Fintype.card S - 1)
⊢ False

...

lean_code_actions

Get LSP code actions for a line. Returns resolved edits for "Try This" suggestions (simp?, exact?, apply?) and other quick fixes. The agent applies the edits using its own editing tools.

{
  "actions": [
    {
      "title": "Try this: simp only [zero_add]",
      "is_preferred": false,
      "edits": [
        {
          "new_text": "simp only [zero_add]",
          "start_line": 3,
          "start_column": 37,
          "end_line": 3,
          "end_column": 42
        }
      ]
    }
  ]
}

lean_get_widgets

Get panel widgets at a position (proof visualizations, #html, custom widgets). Returns raw widget data - may be verbose.

{
  "widgets": [
    {
      "id": "ProofWidgets.HtmlDisplayPanel",
      "javascriptHash": "15661785739548337049",
      "props": {
        "html": {
          "element": ["b", [], [{"text": "Hello widget"}]]
        }
      },
      "range": {
        "start": {"line": 4, "character": 0},
        "end": {"line": 4, "character": 50}
      }
    }
  ]
}

lean_get_widget_source

Get the JavaScript source code of a widget by its javascriptHash (from lean_get_widgets or lean_diagnostic_messages with interactive=True). Useful for understanding custom widget rendering logic. Returns full JS module - may be verbose.

lean_profile_proof

Profile a theorem to identify slow tactics. Runs lean --profile on an isolated copy of the theorem and returns per-line timing data.

{
  "ms": 42.5,
  "lines": [
    {"line": 7, "ms": 38.2, "text": "simp [add_comm, add_assoc]"}
  ],
  "categories": {
    "simp": 35.1,
    "typeclass inference": 4.2
  }
}

lean_verify

Check theorem soundness: returns axioms used + optional source pattern scan for unsafe, set_option debug.*, @[implemented_by], etc. Standard axioms are propext, Classical.choice, Quot.sound - anything else (e.g. sorryAx) indicates an unsound proof. Source warnings require ripgrep (rg).

{
  "axioms": ["propext", "sorryAx"],
  "warnings": [
    {"line": 5, "pattern": "set_option debug.skipKernelTC"}
  ]
}

Local Search Tools

lean_local_search

Search for Lean definitions and theorems in the local Lean project and stdlib. This is useful to confirm declarations actually exist and prevent hallucinating APIs.

This tool requires ripgrep (rg) to be installed and available in your PATH.

External Search Tools

Currently most external tools are separately rate limited to 3 requests per 30 seconds. Please don't ruin the fun for everyone by overusing these amazing free services!

Please cite the original authors of these tools if you use them!

lean_leansearch

Search for theorems in Mathlib using leansearch.net (natural language search).

Github Repository | Arxiv Paper

• Supports natural language, mixed queries, concepts, identifiers, and Lean terms.
• Example: bijective map from injective, n + 1 <= m if n < m, Cauchy Schwarz, List.sum, {f : A → B} (hf : Injective f) : ∃ h, Bijective h

  {
    "module_name": "Mathlib.Logic.Function.Basic",
    "kind": "theorem",
    "name": "Function.Bijective.injective",
    "signature": " {f : α → β} (hf : Bijective f) : Injective f",
    "type": "∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Bijective f → Function.Injective f",
    "value": ":= hf.1",
    "informal_name": "Bijectivity Implies Injectivity",
    "informal_description": "For any function $f \\colon \\alpha \\to \\beta$, if $f$ is bijective, then $f$ is injective."
  },
  ...

lean_loogle

Search for Lean definitions and theorems using loogle.lean-lang.org.

Github Repository

• Supports queries by constant, lemma name, subexpression, type, or conclusion.
• Example: Real.sin, "differ", _ * (_ ^ _), (?a -> ?b) -> List ?a -> List ?b, |- tsum _ = _ * tsum _
• Local mode available: Use --loogle-local to run loogle locally (avoids rate limits, see Local Loogle section)

[
  {
    "type": " (x : ℝ) : ℝ",
    "name": "Real.sin",
    "module": "Mathlib.Data.Complex.Trigonometric"
  },
  ...
]

lean_leanfinder

Semantic search for Mathlib theorems using Lean Finder.

Arxiv Paper

• Supports informal descriptions, user questions, proof states, and statement fragments.
• Examples: algebraic elements x,y over K with same minimal polynomial, Does y being a root of minpoly(x) imply minpoly(x)=minpoly(y)?, ⊢ |re z| ≤ ‖z‖ + transform to squared norm inequality, theorem restrict Ioi: restrict Ioi e = restrict Ici e

Query: Does y being a root of minpoly(x) imply minpoly(x)=minpoly(y)?

  [
    [
      "/-- If `y : L` is a root of `minpoly K x`, then `minpoly K y = minpoly K x`. -/\ntheorem eq_of_root {x y : L} (hx : IsAlgebraic K x)\n    (h_ev : Polynomial.aeval y (minpoly K x) = 0) : minpoly K y = minpoly K x :=\n  ((eq_iff_aeval_minpoly_eq_zero hx.isIntegral).mpr h_ev).symm",
      
      "Let $L/K$ be a field extension, and let $x, y \\in L$ be elements such that $y$ is a root of the minimal polynomial of $x$ over $K$. If $x$ is algebraic over $K$, then the minimal polynomial of $y$ over $K$ is equal to the minimal polynomial of $x$ over $K$, i.e., $\\text{minpoly}_K(y) = \\text{minpoly}_K(x)$. This means that if $y$ satisfies the polynomial equation defined by $x$, then $y$ shares the same minimal polynomial as $x$."
    ],
    ...
  ]

lean_state_search

Search for applicable theorems for the current proof goal using premise-search.com.

Github Repository | Arxiv Paper

A self-hosted version is available and encouraged. You can set an environment variable LEAN_STATE_SEARCH_URL to point to your self-hosted instance. It defaults to https://premise-search.com.

Uses the first goal at a given line and column. Returns a list of relevant theorems.

[
  {
    "name": "Nat.mul_zero",
    "formal_type": "∀ (n : Nat), n * 0 = 0",
    "module": "Init.Data.Nat.Basic"
  },
  ...
]

lean_hammer_premise

Search for relevant premises based on the current proof state using the Lean Hammer Premise Search.

Github Repository | Arxiv Paper

A self-hosted version is available and encouraged. You can set an environment variable LEAN_HAMMER_URL to point to your self-hosted instance. It defaults to http://leanpremise.net.

Uses the first goal at a given line and column. Returns a list of relevant premises (theorems) that can be used to prove the goal.

Note: We use a simplified version, LeanHammer might have better premise search results.

[
  "MulOpposite.unop_injective",
  "MulOpposite.op_injective",
  "WellFoundedLT.induction",
  ...
]

Project-level tools

lean_build

Rebuild the Lean project and restart the Lean LSP server.

Disabling Tools

Many clients allow the user to disable specific tools manually (e.g. lean_build).

VSCode: Click on the Wrench/Screwdriver icon in the chat.

Cursor: In "Cursor Settings" > "MCP" click on the name of a tool to disable it (strikethrough).

MCP Configuration

This MCP server works out-of-the-box without any configuration. However, a few optional settings are available.

Environment Variables

• LEAN_LOG_LEVEL: Log level for the server. Options are "INFO", "WARNING", "ERROR", "NONE". Defaults to "INFO".
• LEAN_LOG_FILE_CONFIG: Config file path for logging, with priority over LEAN_LOG_LEVEL. If not set, logs are printed to stdout.
• LEAN_PROJECT_PATH: Path to your Lean project root. Set this if the server cannot automatically detect your project.
• LEAN_REPL: Set to true, 1, or yes to enable fast REPL-based lean_multi_attempt (~5x faster, see REPL Setup).
• LEAN_REPL_PATH: Path to the repl binary. Auto-detected from .lake/packages/repl/ if not set.
• LEAN_REPL_TIMEOUT: Per-command timeout in seconds (default: 60).
• LEAN_REPL_MEM_MB: Max memory per REPL in MB (default: 8192). Only enforced on Linux/macOS.
• LEAN_LSP_MCP_TOKEN: Secret token for bearer authentication when using streamable-http or sse transport.
• LEAN_STATE_SEARCH_URL: URL for a self-hosted premise-search.com instance.
• LEAN_HAMMER_URL: URL for a self-hosted Lean Hammer Premise Search instance.
• LEAN_LOOGLE_LOCAL: Set to true, 1, or yes to enable local loogle (see Local Loogle section).
• LEAN_LOOGLE_CACHE_DIR: Override the cache directory for local loogle (default: ~/.cache/lean-lsp-mcp/loogle).

You can also often set these environment variables in your MCP client configuration:

{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "uvx",
            "args": [
                "lean-lsp-mcp"
            ],
            "env": {
                "LEAN_PROJECT_PATH": "/path/to/your/lean/project",
                "LEAN_LOG_LEVEL": "NONE"
            }
        }
    }
}

Transport Methods

The Lean LSP MCP server supports the following transport methods:

• stdio: Standard input/output (default)
• streamable-http: HTTP streaming
• sse: Server-sent events (MCP legacy, use streamable-http if possible)

You can specify the transport method using the --transport argument when running the server. For sse and streamable-http you can also optionally specify the host and port:

uvx lean-lsp-mcp --transport stdio # Default transport
uvx lean-lsp-mcp --transport streamable-http # Available at http://127.0.0.1:8000/mcp
uvx lean-lsp-mcp --transport sse --host localhost --port 12345 # Available at http://localhost:12345/sse

Bearer Token Authentication

Transport via streamable-http and sse supports bearer token authentication. This allows publicly accessible MCP servers to restrict access to authorized clients.

Set the LEAN_LSP_MCP_TOKEN environment variable (or see section 3 for setting env variables in MCP config) to a secret token before starting the server.

Example Linux/MacOS setup:

export LEAN_LSP_MCP_TOKEN="your_secret_token"
uvx lean-lsp-mcp --transport streamable-http

Clients should then include the token in the Authorization header.

REPL Setup

Enable fast REPL-based lean_multi_attempt (~5x faster). Uses leanprover-community/repl tactic mode.

1. Add REPL to your Lean project's lakefile.toml:

[[require]]
name = "repl"
git = "https://github.com/leanprover-community/repl"
rev = "v4.25.0"  # Match your Lean version

2. Build it:

lake build repl

3. Enable via CLI or environment variable:

uvx lean-lsp-mcp --repl

# Or via environment variable
export LEAN_REPL=true

The REPL binary is auto-detected from .lake/packages/repl/. Falls back to LSP if not found.

Local Loogle

Run loogle locally to avoid the remote API's rate limit (3 req/30s). First run takes ~5-10 minutes to build; subsequent runs start in seconds.

# Enable via CLI
uvx lean-lsp-mcp --loogle-local

# Or via environment variable
export LEAN_LOOGLE_LOCAL=true

Requirements: git, lake (elan), ~2GB disk space.

Note: Local loogle is currently only supported on Unix systems (Linux/macOS). Windows users should use WSL or the remote API.

Falls back to remote API if local loogle fails.

Notes on MCP Security

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

This MCP server 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 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.

Development

MCP Inspector

npx @modelcontextprotocol/inspector uvx --with-editable path/to/lean-lsp-mcp python -m lean_lsp_mcp.server

Run Tests

uv sync --all-extras
uv run pytest tests

Publications and Formalization Projects using lean-lsp-mcp

• Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics arxiv
• Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics arxiv github
• MerLean: An Agentic Framework for Autoformalization in Quantum Computation arxiv
• M2F: Automated Formalization of Mathematical Literature at Scale arxiv
• A Group-Theoretic Approach to Shannon Capacity of Graphs and a Limit Theorem from Lattice Packings github

Talks

lean-lsp-mcp: Tools for agentic interaction with Lean (Lean Together 2026) youtube

Related Projects

• LeanTool
• LeanExplore MCP

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