Metadata-Version: 2.4
Name: lean-probe
Version: 0.4.0
Summary: Fast Lean 4 proof feedback for agents, powered by LeanInteract.
Author: LeanProbe contributors
License-Expression: MIT
Project-URL: Homepage, https://github.com/Lemmy00/LeanProbe
Project-URL: Documentation, https://github.com/Lemmy00/LeanProbe#readme
Project-URL: Issues, https://github.com/Lemmy00/LeanProbe/issues
Project-URL: Source, https://github.com/Lemmy00/LeanProbe
Keywords: Lean,Lean 4,theorem proving,MCP,agents,LeanInteract
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Libraries :: Python Modules
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: lean-interact<1,>=0.11.0
Requires-Dist: mcp<2,>=1.2.0
Provides-Extra: mcp
Provides-Extra: dev
Requires-Dist: build; extra == "dev"
Requires-Dist: mypy; extra == "dev"
Requires-Dist: pre-commit; extra == "dev"
Requires-Dist: pytest; extra == "dev"
Requires-Dist: pytest-xdist; extra == "dev"
Requires-Dist: ruff; extra == "dev"
Requires-Dist: twine; extra == "dev"
Dynamic: license-file

# LeanProbe

[![PyPI](https://img.shields.io/pypi/v/lean-probe.svg)](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.
