lean-mcp

MCP server and client for Lean 4 + Mathlib formal theorem verification.

Exposes the Lean 4 compiler as an MCP tool (verify_lean_theorem) via stdio transport, allowing any MCP-compatible AI client (OpenCode, Claude Desktop, Cursor, etc.) to verify mathematical proofs.

Prerequisites

• Lean 4 installed via Elan
• A Lean 4 project with Mathlib dependency (with lake build completed)
• Python 3.10+

Installation

pip install lean-mcp

Or install from source:

git clone https://github.com/KrystianYCSilva/lean-mcp.git
cd lean-mcp
pip install -e .

Quick Start

Server

Run the MCP server (stdio transport):

LEAN_PROJECT_PATH=/path/to/your/lean4/project lean-mcp-server

Client (Programmatic)

import asyncio
from lean_mcp.client import LeanMCPClient

async def main():
    async with LeanMCPClient() as client:
        await client.connect(lean_project_path="/path/to/lean4/project")

        result = await client.verify(
            "theorem modus_ponens (P Q : Prop) (hp : P) (hpq : P -> Q) : Q := hpq hp"
        )
        print(result)  # [QED] Compilacao bem-sucedida. Nenhum erro. Prova completa.

asyncio.run(main())

Client Configuration (Claude Desktop, OpenCode, etc.)

Add to your MCP client configuration:

{
  "mcpServers": {
    "lean-mcp": {
      "command": "lean-mcp-server",
      "env": {
        "LEAN_PROJECT_PATH": "/absolute/path/to/lean4/project"
      }
    }
  }
}

Tool: verify_lean_theorem

Parameter	Type	Required	Description
lean_code	string	yes	Lean 4 code to compile. If no import is present, import Mathlib is prepended automatically.
timeout	int	no	Compilation timeout in seconds (default: 120).

Return Values

Prefix	Meaning
[QED]	Proof compiles successfully (returncode 0, no output).
[FEEDBACK DO COMPILADOR]	Compilation error — includes compiler output for debugging.
[ERRO_SISTEMA]	Infrastructure failure (timeout, lake not found, etc.).

Architecture

MCP Client (any)
    |
    | stdio (JSON-RPC)
    v
lean_mcp/server.py      Tool: verify_lean_theorem
    |
    | subprocess (lake env lean)
    v
Lean 4 + Mathlib         Formal verifier

Environment Variables

Variable	Required	Description
LEAN_PROJECT_PATH	yes	Absolute path to the Lean 4 project directory containing lakefile.toml.

License

MIT