About Lean MCP
Lean MCP is an MCP server published by KrystianYCSilva in the Developer Tools category: mCP server and client for Lean 4 + Mathlib formal theorem verification.
Six months or more without a commit doesn't mean the server is broken, but check the open issues before depending on it in production.
Install
git clone https://github.com/KrystianYCSilva/lean-mcpThis server has no ConduID identity, so agent calls to it are not receipted. Pin the version you install and review the source before granting it credentials.
Ask AI
Ask AI about Lean MCP
Powered by Claude · Grounded in docs
Security checks
- ✓README presentThe repository ships documentation.
- ✓License declaredUsable under a stated license.
- !Scoped permissionsDoesn't declare a permission scope. Assume it can do anything its process can.
3 checks have not been run yet.
README
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 buildcompleted) - 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
README copy captured when this server was indexed; it may lag the repository. The original is authoritative.