LeanProbe

LeanProbe

[](https://pypi.org/project/lean-probe/)

Fast Lean 4 proof feedback for AI agents — an MCP server, CLI, and Python API.

LeanProbe keeps a Lean REPL warm and reuses the elaborated environment, so repeated checks in a file come back in tens of milliseconds instead of the seconds a fresh lake build or lake env lean costs. It never edits files — run lake build as the final whole-project gate. Built on LeanInteract.

Quickstart

Install (the MCP server is included):

pip install lean-probe          # or run with no install: uvx lean-probe mcp

Add it to Claude Code:

claude mcp add lean-probe --env LEAN_PROBE_AUTO_BUILD=0 -- lean-probe mcp

Now ask the agent to check Lean — e.g. "use lean_check on theorem t : 2 + 2 = 4 := by norm_num". Or straight from the terminal:

lean-probe check --cwd /path/to/lake-project --code "example : 2 + 2 = 4 := rfl"

That is the whole regular setup — pip install lean-probe is fully functional on its own and writes nothing outside its own package.

Optional — install the usage skill. So your agents know the LeanProbe tool contract without you pasting it, you can additionally install it as a skill. It ships inside the wheel (no repo clone), and this step is purely opt-in — a plain pip install never touches ~/.claude or ~/.codex:

lean-probe install-skill        # → ~/.claude/skills + ~/.codex/skills (whichever exist)

This drops the [LeanProbe skill](src/lean_probe/skill/SKILL.md) into each present client as skills/lean-probe/SKILL.md. Use --client claude|codex to force one, --skills-dir PATH for a project-local .claude/skills, or --dry-run to preview. The skill only documents the tools — keep the claude mcp add / Codex config above so the lean-probe MCP server is actually connected.

Requirements

• Python 3.10+.
• Lean 4 + Lake via elan, with lake on

PATH (or set LEAN_PROBE_LAKE_PATH).

• A built Lake project to check against (with Mathlib if your code imports it).

The first call boots the REPL and elaborates imports (tens of seconds for Mathlib); after that, checks are sub-second — call lean_status with warm=true to pay that cost up front. Keep LEAN_PROBE_AUTO_BUILD=0 for MCP clients: build output on stdout would corrupt the JSON-RPC stream, so build the project from a terminal first.

Add to other clients

Codex (~/.codex/config.toml):

[mcp_servers.lean-probe]
command = "lean-probe"
args = ["mcp"]
tool_timeout_sec = 600          # the first Mathlib call is slow

[mcp_servers.lean-probe.env]
LEAN_PROBE_AUTO_BUILD = "0"

Any MCP client (generic mcpServers JSON):

{
  "mcpServers": {
    "lean-probe": { "command": "lean-probe", "args": ["mcp"], "env": { "LEAN_PROBE_AUTO_BUILD": "0" } }
  }
}

If the client launches the server outside your environment, use an absolute path to lean-probe, or "command": "uvx", "args": ["lean-probe", "mcp"].

Tools

On connect the server advertises usage instructions and exposes six tools:

| Tool | Purpose | |---|---| | lean_check | Verify any standalone snippet — the default. | | lean_check_target | Check or replace a declaration in a project file (warm, sub-second). | | lean_status | Readiness; warm=true pre-boots the REPL. | | lean_proof_state · lean_tactic · lean_close_proof | Explore a sorry tactic by tactic. |

Read a result with two fields: success = the tool ran; ok = Lean accepted the code (no errors, no sorry). On failure, error_code + hint say what to do next. See the [LeanProbe skill](src/lean_probe/skill/SKILL.md) for the full contract — parameters, feedback_lean, and every error code.

Without MCP

CLI:

lean-probe status --cwd /path/to/lake-project
lean-probe check-target File.lean my_theorem --cwd /path/to/lake-project --pretty

Python:

from lean_probe import LeanProbe

probe = LeanProbe()
result = probe.check_target("File.lean", theorem_id="my_theorem", cwd="/path/to/lake-project")
print(result["ok"], result["elapsed_s"])

Benchmarks

Warm cached checks run in tens of milliseconds versus roughly 2–4s for a full-file Lake check — about 9–14× faster for sequential same-file work. See [BENCHMARKS.md](BENCHMARKS.md) for methodology and full numbers.

More

• [SKILL.md](src/lean_probe/skill/SKILL.md) — the full MCP contract (using

LeanProbe), installable into agents with lean-probe install-skill.

• [AGENTS.md](AGENTS.md) — the contributor guide (working on this repo).
• [BENCHMARKS.md](BENCHMARKS.md) — benchmark methodology and results.
• [CONTRIBUTING.md](CONTRIBUTING.md) — dev setup and checks.

Source & license

This open-source MCP server is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: epfl-lara
• Source: epfl-lara/LeanProbe
• License: MIT

Install and usage instructions live in the source repository linked above.