对 Lean4 的批判性审视
A critical look at Lean4
AI 导读
LessWrong 用户 Milo Moses 发表文章，批判性审视形式化证明工具 Lean4 的可信度。他指出 Lean4 基于自研的依赖类型论而非 ZFC，目前没有公开证明其相对于 ZFC 加任意大基数公理是一致的，并称自己 90% 确信当前 GitHub 上的 Lean4 存在一个会被社区视为 bug 的 True=False 证明。文章提到 Lean FRO 在 soundness bug #14576 后又发现七个内核 bug，Leo de Moura 称 AI 很擅长利用内核的 soundness bug，嵌套归纳类型研究尚处早期、可能带来一致但行为失控的隐患。作者还批评 Anthropic 在费马大定理形式化中运行 comparator 时关闭了隔离不可信证明代码的沙箱，并称让 GPT-6 Astra 寻找 Lean4 到集合论的嵌入，花费约 25 小时和数千美元仍未成功。