lean-agent/README.md

Lean Agent

独立 Python 3.11+ 项目：LLM 生成 tactic → Lean 验证 → 把错误反馈给模型修复。已在 Lean 4.35.0 验证（CI：ubuntu24.04-x64-lean4.35 runner，含 Mathlib v4.35.0），无 Python 运行时第三方依赖。

使用

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；本地服务可以不设密钥。任何非兼容服务可以使用适配器：

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 官方说明。

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

python3 -m unittest discover -s tests -v

配套 Lean Bench。