lean-lsp-mcp

MCP.Pizza Chef: oOo0oOo

Lean is the tool mathematicians and researchers use to write proofs a computer can verify, line by line. This connector lets an assistant see exactly what Lean sees: the goal still to be proved, the error messages, the documentation behind a name, the definitions currently in scope. It can also search reference libraries such as LeanSearch, Loogle and Lean Hammer for a theorem that fits the gap. It works in VS Code, Cursor, Claude Code and Mistral Vibe. No account or key needed.

Coding

Web/Research

Use This MCP server To

See exactly where my proof stops working Ask what goal is still left to prove here Search for an existing theorem that closes the gap Look up what an unfamiliar definition actually means Have my assistant try a proof and check it immediately

README

lean-lsp-mcp

Lean Theorem Prover MCP

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

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

lean-lsp-mcp FAQ

Is this project still maintained?

Yes, and busily. It was updated in the last week or two and is published regularly.

What do I need before it will work?

Lean itself and a project on your machine that builds. Running a build once by hand first avoids timeouts on the first connection.

Do I need a key or an account?

No. You install a small Python launcher, and the theorem search services it reaches are free and open.

Which apps does it work in?

VS Code, Cursor, Claude Code and Mistral Vibe, with a one-click install button for VS Code.

Can I use this to find a theorem I half remember?

Yes. Describe it in words or give the shape of the statement, and it searches several Lean libraries at once.

Is this useful if I do not write Lean?

Not really. Everything here assumes you already have a Lean project you are working on.