极简 Lean agent 仅用 bash 在 Putnam 获满分

arXiv 论文（2610.17331）提出 mini-Lean-agent，一个刻意极简的 Lean 定理证明 agent，模型唯一可见的工具就是 bash。该 agent 在 Putnam 2025 测试中取得 12/12 满分，单题成本仅 1.28 美元。项目开源后在社区走红，其核心观点是现代强模型无需复杂搜索工具和大量脚手架，仅靠 bash 即可完成困难定理证明任务。

2026-10-21 ~ 2026-10-21 · 2 条相关

• mini-Lean-agent：纯 bash 最小 agent 在 Putnam 2025 拿 12/12，单题成本 1.28 美元 — wellecks · 2026-10-21
• 极简 Lean agent 走红：现代模型只用 bash 就能干重活 — wellecks · 2026-10-21