claude-bot
a3021d9c39
ci / test (push) Successful in 1m15s
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6
39 lines
2.1 KiB
Markdown
39 lines
2.1 KiB
Markdown
# Lean Agent
|
||
|
||
独立 Python 3.11+ 项目：LLM 生成 tactic → Lean 验证 → 把错误反馈给模型修复。已在 Lean 4.35.0 验证（CI：ubuntu24.04-x64-lean4.35 runner，含 Mathlib v4.35.0），无 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)。
|