lean4-mcp-proxy

An MCP (Model Context Protocol) server that proxies between AI agents and the Lean 4 language server. It lets agents open Lean files, check for errors, inspect proof goals, and edit documents through the standard MCP tool-calling interface.

Inspired by vsrocq-mcp (PR#1194), an MCP server patch for the Rocq prover, originally authored by Kacper Korban and available at cu1ch3n/vsrocq-mcp.

:warning: Platform support: Tested on Linux. Windows and macOS support is not guaranteed.

Features

• Open files from disk or memory, with automatic Lake workspace detection
• Get diagnostics (errors, warnings) after Lean finishes type-checking
• Query proof goals at any cursor position inside a tactic block
• Edit documents — full replacement or targeted range edits

Tools

Prerequisites

• Rust (edition 2021+)
• Lean 4 (lean on PATH)
• Lake (lake on PATH, included with Lean 4) — only needed for Lake projects

Build

cargo build --release

The binary is at target/release/lean4-mcp-proxy.

Usage

VS Code / Cursor Setup

Step 1: Build the MCP Server

cargo build --release

The binary will be at target/release/lean4-mcp-proxy.

Step 2: Configure MCP Settings

For VS Code with Cline/Roo-Cline:

1. Open VS Code settings (Cmd/Ctrl + ,)
2. Search for "MCP" or navigate to your MCP extension settings
3. Add the server configuration to your MCP settings file (usually .vscode/mcp.json or global settings):

{
  "mcpServers": {
    "lean4-mcp": {
      "command": "/absolute/path/to/lean4-mcp-proxy",
      "args": []
    }
  }
}

For Cursor:

1. Open Cursor Settings → Features → Model Context Protocol
2. Add a new MCP server with:
   • Name: lean4-mcp
   • Command: /absolute/path/to/lean4-mcp-proxy
   • Args: (leave empty for auto-detection)

Step 3: Verify Installation

After restarting your editor, the MCP server should appear in your MCP tools list. You can verify by:

1. Opening a Lean 4 file (.lean)
2. Asking your AI assistant to "list available MCP tools"
3. You should see tools like open_file, get_diagnostics, get_goal_state, etc.

Step 4: Using with Lake Projects

Lake workspaces are auto-detected from lakefile.lean when you open a file. For a default project, use:

{
  "mcpServers": {
    "lean4-mcp": {
      "command": "/absolute/path/to/lean4-mcp-proxy",
      "args": ["--lake-project", "/path/to/your/lake/project"]
    }
  }
}

Environment variables

Protocol

Communicates over stdio using newline-delimited JSON-RPC (MCP protocol version 2024-11-05). The proxy translates MCP tool calls into LSP requests to the Lean 4 language server.