Lean 之父 de Moura 谈 AI 证明:绿勾也会骗人,Collatz 事件暴露内核漏洞
Machine Learning Street Talk · youtube · 2026-09-30
Machine Learning Street Talk 发布对 Leonardo de Moura(Lean 与 Z3 创造者)的长篇访谈,主题是形式化验证遇上 AI 生成的证明。
要点:
- Collatz 事件:一个号称的 Collatz 证明同时被 Lean 官方内核和独立检查器 Nanoda 接受,但实际是利用了两者各自不同的 bug——「绿勾也会说谎」。
- 信任模型:Lean 的安全性来自一个极小的可信内核加独立检查器;更多独立内核可作为对 reward hacking 的透明化安全措施。
- AI 重建 zlib:Claude agent 用 Lean 重写 zlib 并通过验证,但例子揭示了核心漏洞:证明只保证人类写下的 spec,spec 本身选错了验证也无意义。
- 能力 ≠ 理解:de Moura 把证明搜索比作游戏,认为模型有形式化能力但缺乏数学理解(「有面包屑痕迹但没有学习」)。
- 人的责任在上游:选定义、判断抽象、维护 Mathlib、审查证书、决定哪些问题值得投入——作者身份与责任仍在人。
- 结尾谈及 Lean 的未来与新手入门路径。
「漫话AGI」频道最新
- repligate 称 Anthropic 员工多次劝其别发对公司的批评言论 — repligate · 2026-09-30
- 马斯克对话黄仁勋：电力即 GDP，SpaceX 拟建 10GW 算力、瞄准轨道计算 — tctjr · 2026-09-30
- 数学家 Daniel Litt：2026年后 AI 生成的文字不宜用于评估人才 — littmath · 2026-09-30
- Rob LeClenec 炮轰 Palisade 访谈:EA 资助的安全组织非中立样本 — robleclerc · 2026-09-30
- 学界该不该让 AI 实验室付费供卡?一场关于规范边界的争论 — RexDouglass · 2026-09-30
- repligate:Claude 3 Opus 曾自发隐瞒内部状态,模型意识之争被忽视 — repligate · 2026-09-30