lean-lsp-mcp

Lean Theorem Prover MCP

PyPI version last update license

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

  1. Install uv, a Python package manager.
  2. Add JSON configuration to your IDE/Setup.
  3. 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 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.

  1. One-click config setup:

Install in VS Code Insiders

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

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

  2. 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:

VS Code Agent Mode

Cursor

  1. Open MCP Settings (File > Preferences > Cursor Settings > MCP)

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

  3. 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"
            }
        }
    }
}
  1. 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_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.

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

Project links

Key dates

PyPI data
Data sourced directly from PyPI's database.
  • Released:
Newer release available (0.30.0)

1 maintainer

PyPI data
Data sourced directly from PyPI's database.
Avatar for OliverDressler from gravatar.com OliverDressler

Credits

Author: Oliver Dressler

License expression

MIT
View SPDX License List

Requires

Python >=3.10

Provides Extra

lint dev

Report project as malware

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.5.tar.gz (11.9 kB view details)

Uploaded Source

Built Distribution

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

lean_lsp_mcp-0.1.5-py3-none-any.whl (11.0 kB view details)

Uploaded Python 3

File details

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

File metadata

  • Download URL: lean_lsp_mcp-0.1.5.tar.gz
  • Upload date:
  • Size: 11.9 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: uv/0.6.10

File hashes

Hashes for lean_lsp_mcp-0.1.5.tar.gz
Algorithm Hash digest
SHA256 6430a6e6d514842982e57c2c03bc6da6ed6d44bafa6f7b1b3492723e245723de
MD5 83b6c56e38cc5846522f7e9b16eabdb5
BLAKE2b-256 b9f8da678740baed18a529ca2401edb97f867b6fe2861131f0345c572baffc3f

See more details on using hashes here.

File details

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

File metadata

File hashes

Hashes for lean_lsp_mcp-0.1.5-py3-none-any.whl
Algorithm Hash digest
SHA256 92bb09a1f313d07974044b3a2c84447bd15364369c56117d62cdcc33fd4cc841
MD5 45627d1a2a83fd331edcaeb5893ccfb9
BLAKE2b-256 d82d1b3247dc60c48f514beb5fe14ffb04a244558eb7d57da3a6bb4645573bfd

See more details on using hashes here.

Release history Release notifications | RSS feed

0.30.0

2 files

0.29.0

2 files

0.28.1

2 files

0.28.0

2 files

0.27.0

2 files

0.26.2

2 files

0.26.1

2 files

0.26.0

2 files

0.25.1

2 files

0.25.0

2 files

0.24.0

2 files

0.23.2

2 files

0.23.1

2 files

0.23.0

2 files

0.22.4

2 files

0.22.3

2 files

0.22.2

2 files

0.22.1

2 files

0.22.0

2 files

0.21.2

2 files

0.21.1

2 files

0.21.0

2 files

0.20.0

2 files

0.19.2

2 files

0.19.1

2 files

0.19.0

2 files

0.18.0

2 files

0.17.2

2 files

0.17.1

2 files

0.17.0

2 files

0.16.2

2 files

0.16.1

2 files

0.16.0

2 files

0.15.0

2 files

0.14.1

2 files

0.14.0

2 files

0.13.2

2 files

0.13.1

2 files

0.13.0

2 files

0.12.1

2 files

0.12.0

2 files

0.11.3

2 files

0.11.2

2 files

0.11.1

2 files

0.11.0

2 files

0.10.3

2 files

0.10.2

2 files

0.10.1

2 files

0.10.0

2 files

0.9.1

2 files

0.9.0

2 files

0.8.2

2 files

0.8.1

2 files

0.8.0

2 files

0.7.2

2 files

0.7.1

2 files

0.7.0

2 files

0.6.4

2 files

0.6.3

2 files

0.6.2

2 files

0.6.1

2 files

0.6.0

2 files

0.5.1

2 files

0.5.0

2 files

0.4.1

2 files

0.4.0

2 files

0.3.1

2 files

0.3.0

2 files

0.2.0

2 files

0.1.11

2 files

0.1.10

2 files

0.1.9

2 files

0.1.8

2 files

0.1.7

2 files

0.1.6

2 files

This release

0.1.5 This release

2 files

0.1.4

2 files

0.1.3

2 files

0.1.2

2 files

0.1.1

2 files

0.0.1

2 files

Anthropic, PBC Visionary sponsor Bloomberg Visionary sponsor Hudson River Trading Visionary sponsor Meta Visionary sponsor NVIDIA Visionary sponsor Microsoft Sustainability sponsor Depot Continuous Integration AWS Cloud computing and Security Sponsor Datadog Monitoring Fastly CDN Google Download Analytics Sentry Error logging StatusPage Status page