# Lean Agent

独立 Python 3.11+ 项目：LLM 生成 tactic → Lean 验证 → 把错误反馈给模型修复。已在 Lean 4.33.1 验证，无 Python 运行时第三方依赖。

## 使用

```sh
python3 -m venv .venv
source .venv/bin/activate
pip install -e .
printf '%s\n' '{"id":"example","statement":"∀ n : Nat, n = n"}' > /tmp/task.json
export LLM_API_KEY='your-key'
lean-agent /tmp/task.json --model YOUR_MODEL --base-url https://YOUR_HOST/v1
```

HTTP 接口使用 `/chat/completions`；本地服务可以不设密钥。任何非兼容服务可以使用适配器：

```sh
lean-agent /tmp/task.json --provider-command '["python3","/absolute/path/adapter.py"]'
```

适配命令 stdin 接收 `{"messages":[{"role":"user","content":"..."}]}`，stdout 返回 Lean tactic 正文；错误用非零退出码，日志用 stderr。也可实现 Python `Provider.complete(messages) -> str`。任何支持文本输出的 LLM 均可适配，但不保证证明能力。

任务含 id、statement、可选 prelude（如 import Mathlib）。输出记录每轮证明、诊断、耗时。成功退出 0，失败退出 1。

Mathlib 使用已有 Lake 项目：`--lean-project /absolute/project --lean-command '["lake","env","lean"]'`。不自动安装 Mathlib。可用 `--attempts`、`--lean-timeout`、`--llm-timeout` 控制预算。

## 验证与限制

拒绝 sorry/admit 和常见命令注入；要求编译成功、无 warning，并通过 #print axioms 确认仅依赖 propext、Classical.choice、Quot.sound 或无公理。[Lean 官方说明](https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/)。

文本过滤不是安全沙箱。数据集/prelude、导入模块、适配器必须可信；不可信模型代码应在无密钥、无网络、限制资源的容器或虚拟机中运行。当前仅提供进程超时和 Lean heartbeat 限制。不包含交互式 goal 搜索、token 计费。

```sh
python3 -m unittest discover -s tests -v
```

配套 [Lean Bench](https://gitea.entroia.com/codex-bot/lean-bench)。