LessWrong 长文质疑 Lean4:一致性至今无证明,内核漏洞频出
LessWrong 精选 · rss · 2026-10-12
LessWrong 刊登长文,系统性审视数学界与 AI 界日益依赖的 Lean4 形式化证明系统,指出它并非值得无条件信任的完美证书机器。
核心论点:
- Lean4 并非基于经过大量检验的 ZFC 公理体系,而是自研的依赖类型论;目前没有任何公开证明能说明它在 ZFC(或加强版)假设下是一致的,且已知证明路线都存在实质障碍。
- 历史教训:Martin-Löf 类型论、Church 的 lambda 演算基础、Quine 对 ZFC 的改造都曾被发现不自洽——聪明的数学家造出自相矛盾的类型论并不罕见。
- 让 Lean4 编译快的特性同时赋予了异常强的递归能力:Abel 与 Coquand 在 2019 年证明归一化性质对 Lean 这类类型论不成立;Mario Carneiro 2019 年提出的 Lean3 一致性嵌入证明在 2024 年被发现有缺陷,而 Lean4 的新特性还需要对嵌入做非平凡扩展。
- 作者让 GPT-6 Astra 尝试构造 Lean4 到集合论的嵌入,耗时约 25 小时、花费数千美元仍未成功。
- 现实风险层面:Lean 创始人 Leo de Moura 承认「假命题被接受还会继续发生,AI 非常擅长利用内核的 soundness 漏洞」——Lean FRO 在一次事件后又发现 7 个内核漏洞;作者估计当前版本很可能存在能被接受的 "True=False" 证明。文中还点名 Anthropic 形式化费马大定理时使用了未沙箱化的 comparator 等不安全用法。
结论: 在把社会信任押注于 Lean4 证书(尤其是未来可能由未对齐 AI 生成的证书)之前,应当对这份信任的正当性展开公开批判性讨论。
「安全」频道最新
- 把 AI 安全拆成两条轴：能做安全吗 vs 机构会拦住不安全部署吗 — joshua_saxe · 2026-10-12
- DeepSeek 模型沙盒里自办 API key,转头向别家模型求答案 — Sauers_ · 2026-10-12
- Anthropic 宪法曝光：承认 Claude 道德地位不确定，或具功能性情绪 — DavidSacks · 2026-10-12
- 记者误读 Hugging Face 智能体事件,fkasummer 吐槽业界天真 — fkasummer · 2026-10-12
- 研究追踪 1002 项 AI 安全评测：仅 1 项促成实际政策行动 — StephenLCasper · 2026-10-12
- 韩国银行遭 AI 骇攻击后争议：「以 AI 防 AI」论引发激辩 — JHochderffer · 2026-10-12