lean-lsp-mcp

What it is and what it does

lean-lsp-mcp is an MCP (Model Context Protocol) server that bridges the Lean theorem prover and LLM agents by exposing Lean's language server capabilities as a set of tools. It runs as a stdio-based service that agents can invoke to inspect proof states, retrieve diagnostics, search for theorems and definitions, and interact with Lean projects programmatically.

The package wraps leanclient to communicate with Lean's LSP, and provides tools for goal inspection, term information, hover documentation, and external theorem search via services like Loogle and Lean Hammer. It integrates with IDEs (VSCode, Cursor, Claude Code, Mistral Vibe) and supports optional features like REPL-based code execution and ripgrep-powered local search. Configuration is minimal—the server works out-of-the-box but allows customization via environment variables for logging, tool disabling, and performance tuning.

Use it for:

• Enable Claude Code or other agentic IDEs to assist with Lean 4 theorem proving by providing real-time proof state and diagnostic information.
• Automate theorem discovery and proof search by querying external databases like Loogle and Lean Hammer through a unified interface.
• Build custom agents that analyze Lean projects, extract goal states, and suggest relevant theorems or lemmas for proof completion.
• Integrate Lean proof verification into LLM-based code generation workflows where formal correctness is required.
• Provide local search capabilities for Lean definitions and theorems using ripgrep for faster development iteration.

Worth the install?

AI-flagged interpretation of the facts on this page — verify before relying

Provides an MCP server that exposes the Lean theorem prover to LLM agents via the Language Server Protocol, enabling programmatic access to proof states, diagnostics, and theorem search tools.

Yes. The package is actively maintained, has low install friction, carries no known vulnerabilities, and uses a permissive MIT license. It is purpose-built for integrating Lean with LLM agents and IDEs—if you are working with Lean 4 projects and want agentic proof assistance, this is the standard tool. Install it if you use Cursor, Claude Code, or similar platforms with Lean projects.

Install

lean-lsp-mcp on PyPI

pip install lean-lsp-mcp

uv add lean-lsp-mcp

poetry add lean-lsp-mcp

Installing lean-lsp-mcp

Before you install

Low install friction with a pure Python wheel and four runtime dependencies. Active maintenance with a recent release 17 days ago and 475 repository stars indicate ongoing development.

License in practice

MIT license permits unrestricted use, modification, and distribution with minimal restrictions, making it suitable for both open-source and commercial projects.

Quickstart

pip install lean-lsp-mcp

# Configure in your IDE (e.g., VSCode mcp.json):
# {
#   "servers": {
#     "lean-lsp": {
#       "type": "stdio",
#       "command": "uvx",
#       "args": ["lean-lsp-mcp"]
#     }
#   }
# }

# Or run directly:
uvx lean-lsp-mcp

Requires Python >=3.10, a Lean project with lakefile.toml or lakefile.lean, and the Lean toolchain (elan/lake) installed. Running `lake build` before starting the MCP is recommended to avoid timeouts.

Verify before relying

• Whether all external search tools (LeanSearch, Loogle, Lean Finder, Lean Hammer, Lean State Search) are functional without additional setup or API keys.
• Performance characteristics when handling large Lean projects or concurrent agent requests.
• Compatibility with Lean versions beyond the current toolchain.

Package facts

Evidence: lean_lsp_mcp-0.29.0-py3-none-any.whl

Tags

More Artificial Intelligence packages

Further reading