FORALL-LEAN-AGENT 把 Lean agent 的“通过编译”升级为可审计 acceptance chain

Lwin 提出 FORALL-LEAN-AGENT，一个面向 Lean coding agents 的 frontend-agnostic 审计框架。它将隔离工作区、Lean 工具、fresh review、statement comparison、axiom audit 与可用时的 independent proof checking 绑定到同一个 candidate artifact，使 acceptance decision 可追溯，而不把“成功编译”直接等同于“证明了预期命题”。论文在 VeriSoftBench、PutnamBench 和 Lean Eval software-verification track 上评测；在 100-task VeriSoftBench subset 中，GPT-5.6 Sol 的 benchmark-rule success 从 93 提升到 100，同时报告成本从 69 美元降到 62 美元；PutnamBench 672 题全部通过框架 acceptance，平均每题 4.72 美元。