内容
# LeanProbe
[](https://pypi.org/project/lean-probe/)
用于 AI 代理的快速 Lean 4 证明反馈 - 一个 MCP 服务器、命令行界面和 Python API。
LeanProbe 保持 Lean REPL 热启动并重用精化的环境，因此文件中的重复检查在几十毫秒内返回，而不是像新鲜的 `lake build` 或 `lake env lean` 需要的几秒钟。它从不编辑文件 - 将 `lake build` 作为最终的整个项目检查。在 [LeanInteract](https://github.com/augustepoiroux/LeanInteract) 上构建。
## 快速入门
安装（包括 MCP 服务器）：
```bash
pip install lean-probe # 或运行无需安装：uvx lean-probe mcp
```
将其添加到 **Claude Code**：
```bash
claude mcp add lean-probe --env LEAN_PROBE_AUTO_BUILD=0 -- lean-probe mcp
```
现在询问代理检查 Lean - 例如 *"use lean_check on `theorem t : 2 + 2 = 4 := by norm_num`"*. 或直接从终端：
```bash
lean-probe check --cwd /path/to/lake-project --code "example : 2 + 2 = 4 := rfl"
```
这就是整个常规设置 - `pip install lean-probe` 本身完全功能正常，不会写入除其自身软件包以外的任何内容。
**可选 - 安装使用技能。** 这样您的代理可以了解 LeanProbe 工具合约，而无需您复制粘贴，您还可以将其作为技能安装。它包含在 wheel 中（无需仓库克隆），此步骤纯粹是可选的 - 普通的 `pip install` 永远不会触及 `~/.claude` 或 `~/.codex`：
```bash
lean-probe install-skill # → ~/.claude/skills + ~/.codex/skills （两者存在时）
```
这将 [LeanProbe 技能](src/lean_probe/skill/SKILL.md) 放入每个现有客户端，名为 `skills/lean-probe/SKILL.md`. 使用 `--client claude|codex` 强制使用其中一个，使用 `--skills-dir PATH` 表示项目本地的 `.claude/skills`，或使用 `--dry-run` 预览。该技能仅记录工具 - 保留上述 `claude mcp add` / Codex 配置，以便实际连接 `lean-probe` MCP 服务器。
## 要求
- Python 3.10+。
- 通过 [elan](https://github.com/leanprover/elan) 使用 Lean 4 + Lake，`lake` 在 `PATH` 中（或设置 `LEAN_PROBE_LAKE_PATH`）。
- 一个已构建的 Lake 项目，用于检查（如果您的代码导入它，则使用 Mathlib）。
第一次调用将启动 REPL 并精化导入（Mathlib 需要几十秒）；之后，检查将小于一秒 - 调用 `lean_status` 时使用 `warm=true` 来提前支付此费用。 对于 MCP 客户端，请保持 `LEAN_PROBE_AUTO_BUILD=0`：构建输出到 stdout 会损坏 JSON-RPC 流，因此请先从终端构建项目。
## 添加到其他客户端
**Codex** (`~/.codex/config.toml`）：
```toml
[mcp_servers.lean-probe]
command = "lean-probe"
args = ["mcp"]
tool_timeout_sec = 600 # 首次 Mathlib 调用较慢
[mcp_servers.lean-probe.env]
LEAN_PROBE_AUTO_BUILD = "0"
```
**任何 MCP 客户端**（通用 `mcpServers` JSON）：
```json
{
"mcpServers": {
"lean-probe": { "command": "lean-probe", "args": ["mcp"], "env": { "LEAN_PROBE_AUTO_BUILD": "0" } }
}
}
```
如果客户端在您的环境之外启动服务器，请使用 `lean-probe` 的绝对路径，或 `"command": "uvx", "args": ["lean-probe", "mcp"]`.
## 工具
连接时，服务器会提供使用说明并暴露六种工具：
| 工具 | 用途 |
|---|---|
| `lean_check` | 验证任何独立的代码片段 - 默认。 |
| `lean_check_target` | 检查或替换项目文件中的声明（热启动，低于一秒）。 |
| `lean_status` | 就绪状态；`warm=true` 预启动 REPL。 |
| `lean_proof_state` · `lean_tactic` · `lean_close_proof` | 探索 `sorry` 战术，逐战术。 |
读取结果时包含两个字段： **`success`** = 工具已运行； **`ok`** = Lean 接受代码（无错误，无 `sorry`）。如果失败，`error_code` + `hint` 会告知下一步操作。有关完整合约 - 参数、`feedback_lean` 和每个错误代码，请参见 [LeanProbe 技能](src/lean_probe/skill/SKILL.md)。
## 无 MCP
命令行界面：
```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"])
```
## 基准测试
热缓存检查运行在几十毫秒内，而完整的 Lake 检查大约需要 2-4 秒 - 对于顺序的相同文件工作，大约快 9-14 倍。有关方法和完整数字，请参见 [BENCHMARKS.md](BENCHMARKS.md)。
## 更多
- [SKILL.md](src/lean_probe/skill/SKILL.md) - 完整的 MCP 合约（使用 LeanProbe），可使用 `lean-probe install-skill` 安装到代理中。
- [AGENTS.md](AGENTS.md) - 贡献者指南（在此仓库上工作）。
- [BENCHMARKS.md](BENCHMARKS.md) - 基准测试方法和结果。
- [CONTRIBUTING.md](CONTRIBUTING.md) - 开发设置和检查。
