# LeanProbe

> Fast Lean 4 proof feedback for coding agents. CLI, Python library, and MCP server with warm LeanInteract sessions and cached env reuse.

- **Type:** MCP server
- **Install:** `agentstack add mcp-epfl-lara-leanprobe`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [epfl-lara](https://agentstack.voostack.com/s/epfl-lara)
- **Installs:** 0
- **Category:** [Integrations](https://agentstack.voostack.com/c/integrations)
- **Latest version:** 0.1.0
- **License:** MIT
- **Upstream author:** [epfl-lara](https://github.com/epfl-lara)
- **Source:** https://github.com/epfl-lara/LeanProbe

## Install

```sh
agentstack add mcp-epfl-lara-leanprobe
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# 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](https://github.com/augustepoiroux/LeanInteract).

## Quickstart

Install (the MCP server is included):

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

Add it to **Claude Code**:

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

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

```bash
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](https://github.com/leanprover/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`):

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

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

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

Python:

```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](https://github.com/epfl-lara)
- **Source:** [epfl-lara/LeanProbe](https://github.com/epfl-lara/LeanProbe)
- **License:** MIT

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

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** yes
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/mcp-epfl-lara-leanprobe
- Seller: https://agentstack.voostack.com/s/epfl-lara
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.