mini-Lean-agent 用 bash-only 通用 coding agent 挑战专用 theorem-proving harness：Astra 在 Putnam 2025 上 12/12

Ortega 等提出 mini-Lean-agent：把 formal theorem proving agent 压缩成一个通用 coding-agent loop，模型可见工具只有 bash；模型自己读写仓库、搜索本地 Lean library、调用 Lean 并管理中间状态，最终结果则由独立 trusted evaluator 使用 Lean FRO Comparator 验证。论文在 Putnam 2025 的 12 道题上比较 minimal harness 与 AxProverBase / Numina-Lean-Agent：Gemini 3.8 Flash 在每题 2 美元限制下用 mini-Lean-agent 解出 7/12，而 AxProverBase 解出 4/12；使用 Astra 时 mini-Lean-agent 达到 12/12，平均成本 1.28 美元/题。作者主张以后评测 theorem-proving infrastructure 应至少与这种极简通用 coding-agent baseline 比较，以区分 base-model 能力和 specialized harness 的真实增益。