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.

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

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.4.tar.gz (11.2 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.4-py3-none-any.whl (10.0 kB view details)

Uploaded Python 3

File details

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

File metadata

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

File hashes

Hashes for lean_lsp_mcp-0.1.4.tar.gz
Algorithm Hash digest
SHA256 ccad6534ba280b9394a512822baa3a525b2d2e83e13cad879f72d3568c8fe187
MD5 18d42fe80a021863f90b62846aff32e1
BLAKE2b-256 e489a36d17263f0e8c234af41fa80c9bfd0c42718899bbfdcb7e196629798e59

See more details on using hashes here.

File details

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

File metadata

File hashes

Hashes for lean_lsp_mcp-0.1.4-py3-none-any.whl
Algorithm Hash digest
SHA256 7016880b40b8da4d1c5c1992407b52bbc8dc89797ffb97cc45c6d2792d1dba50
MD5 615e7edef59191d5f7fa4923bb4902db
BLAKE2b-256 4aabd4003abf24bb7080f319a2fa5c01d6ff8e6b145dcf048aa5d5c10da2d0fb

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

0.1.5

2 files

This release

0.1.4 This release

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