事件观察中
LessWrong 文章质疑 Lean4 形式化证明可靠性
先了解这件事
AI 综述
2026年10月12日，LessWrong 用户 Milo Moses 发表文章，批判性审视形式化证明工具 Lean4 的可信度。他指出，Lean4 基于自研的依赖类型论而非 ZFC，目前没有公开证明其相对于 ZFC 加任意大基数公理是一致的；并称自己 90% 确信当前 GitHub 上的 Lean4 存在一个会被社区视为 bug 的 True=False 证明。文章还提到，Lean FRO 在 soundness bug #14576 后又发现了七个内核 bug。
AI 根据报道生成 · 1 天前更新
最新进展
对 Lean4 的批判性审视后续时间线
10月9日
- LessWrong对 Lean4 的批判性审视
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 小时和数千美元仍未成功。
相关讨论
关注度走势
每天新增来源
- 10月12日新增1个来源（1家媒体、0个账号）
- 10月13日新增0个来源（0家媒体、0个账号）