oOo0oOo/lean-lsp-mcp

lean‑lsp‑mcp – an MCP server for the Lean theorem prover

What it is – A Python‑based Model Context Protocol (MCP) server that sits on top of the Lean 4 language server. It exposes Lean’s diagnostics, goals, hover info and a suite of search tools (LeanSearch, Loogle, Lean Finder, Lean Hammer) as tools that LLM agents (Claude Code, Cursor, Mistral Vibe, etc.) can call. In short, it lets an LLM talk to a Lean project as if it were a code‑assistant.

Key capabilities

• Query Lean diagnostics, current proof goals, term definitions, hover docs.
• Run external search services (LeanSearch, Loogle, Lean Finder, Lean Hammer) to locate relevant theorems.
• Optional REPL‑backed lean_run_code for fast code execution.
• Configurable via environment variables or MCP client JSON (VS Code, Cursor, Claude Code, Mistral Vibe).
• Supports three transports: stdio (default), streamable‑http, and legacy sse.
• Works with OpenAI’s Secure MCP Tunnel for safe remote access.

How to get it running

1. Install the uv Python package manager (or use Nix).
2. Ensure your Lean project builds (lake build).
3. Install optional tools – ripgrep for local search, repl package for fast code runs, and optionally a local Loogle binary.
4. Add a server entry to your MCP‑aware IDE (VS Code, Cursor, Claude Code, Mistral Vibe) – most examples are a one‑liner that runs uvx lean‑lsp‑mcp.
5. (Optional) Set environment variables to tweak logging, disable specific tools, adjust time‑outs, or enable authentication.

Typical workflow

• An LLM sends a request like “What is the current goal in MyProof.lean?”.
• The MCP server calls the Lean LSP, extracts the goal state, and returns a concise text block.
• For a missing lemma, the LLM can invoke lean_loogle or lean_search which query remote or local indexes and return matching theorems.
• If the LLM wants to try a proof step, it can call lean_run_code (REPL mode) or lean_multi_attempt to test snippets.

Security notes

• The server can read any file inside the project, run builds, and reach the network for search tools, so it should be run in a trusted environment or containerized (Docker image provided).
• When exposing via HTTP, set LEAN_LSP_MCP_TOKEN for bearer‑token auth, or use OpenAI’s Secure MCP Tunnel.

Who uses it

• Researchers building agentic theorem‑proving systems (e.g., Ax‑Prover, Numina‑Lean‑Agent, MerLean, M2F) cite this tool.
• It is presented at conferences such as Lean Together 2026.

Where to find more

• PyPI package: lean-lsp-mcp
• Source code & docs: https://github.com/oOo0oOo/lean-lsp-mcp
• Full tool list in docs/tools.md
• Adding new tools is documented in docs/adding-a-tool.md.

License – MIT (citation appreciated but not required).