# 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](https://github.com/leanprover/elan)
- A **Lean 4 project** with Mathlib dependency (with `lake build` completed)
- **Python 3.10+**

## Installation

```bash
pip install lean-mcp
```

Or install from source:

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

## Quick Start

### Server

Run the MCP server (stdio transport):

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

### Client (Programmatic)

```python
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:

```json
{
  "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