mcplist
LE

lean-lsp-mcp

Created 5 months ago

Lean LSP MCP server for agentic interaction with the Lean theorem prover.

Visit Homepage
development documentation public lean language server

What is lean-lsp-mcp?

Interact with the [Lean theorem prover](https://lean-lang.org/) via the Language Server Protocol.

Documentation

Key Features

  • Rich Lean Interaction: Access diagnostics, goal states, term information, hover documentation and more.
  • External Search Tools: Use leansearch, loogle, 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

  1. Install uv, a Python package manager.
  2. Make sure your Lean project builds quickly by running lake build manually.
  3. Configure your IDE/Setup

Transport Methods

The Lean LSP MCP server supports the following transport methods:

  • stdio: Standard input/output (default)
  • streamable-http: HTTP streaming
  • sse: Server-sent events (MCP legacy, use streamable-http if possible)

Bearer Token Authentication

Transport via streamable-http and sse supports bearer token authentication. Set the LEAN_LSP_MCP_TOKEN environment variable to a secret token before starting the server.

Environment Variables

Some features and integrations of lean-lsp-mcp are configured using environment variables. These must be set in your shell or process environment before running the server.

Server Config 

{
  "mcpServers": {
    "lean-lsp-mcp-server": {
      "command": "npx",
      "args": [
        "lean-lsp-mcp"
      ]
    }
  }
}

Links & Status

Repository: github.com
Hosted: No
Global: No
Official: No

Project Info

Hosted Featured
Created At: Jul 02, 2025
Updated At: Aug 07, 2025
Author: Oliver Dressler
Category: community
License: MIT
Tags:
development documentation public