Skip to main content
Glama
Sign In
lean-mcp

lean-mcp

by KrystianYCSilva
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Local

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+

Related MCP server: prova-mcp

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

Tool Schema Changelog

Recent tool additions, removals, and schema changes observed during successful MCP inspections.

Loading tool schema changelog…

    This server cannot be deployed

    Claude Code, inside the Godot 4 editorFlockbay puts an AI agent in the real Godot 4 editor: it writes GDScript, runs your game and fixes what breaks. Free, or bring your own Claude Code or Codex.flockbay.comAd

    Maintenance

    ActivityInactive
    ResponsivenessNo recent community issues

    Resources

    Related MCP Connectors

    Related MCP Servers

    • Lean MCP

      HyoAkira
      A
      license
      A
      quality
      C
      maintenance
      Enables compiling Lean 4 proof snippets on the local machine against a Mathlib project and returns structured compiler feedback — status, one-line hints, and the compiler's real error, warning, and information messages — so a model can iterate on proofs instead of guessing. Compilation is serialized, timeouts kill stuck tactics, and rejected code is reported as a normal result rather than a tool failure.
      1
      GPL 3.0