Lean 创始人 Leonardo de Moura：一份据称的证明如何疑似利用不同漏洞骗过两个独立内核
Machine Learning Street Talk 播客 2026 年 9 月 30 日一期，Lean 定理证明器创始人 Leonardo de Moura 讲述 Collatz 证明事件中两个独立检查器分别被不同漏洞欺骗的过程，以及小可信内核与独立校验器的架构设计。
一份声称证明了 Collatz 猜想的 Lean 代码，同时通过了 Lean 官方内核和另一个独立检查器 Nanoda 的验证——但似乎各自利用了不同的漏洞使其通过。这是 Lean 定理证明器创始人 Leonardo de Moura 在 2026 年 9 月 30 日 Machine Learning Street Talk 播客中讲述的事件。节目由 Tim Scarfe 主持，时长七十四分钟。
节目从 Lean 为何刻意保持极小的可信内核讲起，延伸到独立检查器的设计初衷与局限。De Moura 讨论了更多检查器的引入、奖励黑客风险以及通过透明性实现安全等议题，并回应了谁控制 Lean 核心这一治理问题。
de Moura 于 2013 年在微软研究院创建了 Lean，最初目的是检查软件代码的正确性；他同时也是 SMT 求解器 Z3 的共同创建者。据 Science News 的书评介绍，如今数学家和 AI 研究者反而成为 Lean 最活跃的使用者。本期节目还涉及 Lean 从 Lean 1 到 Lean 4 的演进、依赖类型与 Mathlib 如何让形式化证明对职业数学家变得可用、AI 智能体在证明搜索中的角色（"面包屑"而非学习）、以及 AlphaProof 和大语言模型时代证书为何仍然重要等话题。
需要说明的是，以上关于 Collatz 事件和内核话题的描述来自节目官方 show notes 的摘要，而非逐字稿。de Moura 的具体论证、对治理模式的判断以及对 AI 智能体局限的分析，需要收听完整节目才能评估。对于关注形式化验证、AI 生成证明的可靠性、以及"自动检查"能否真正替代人类审查的读者，这期节目提供了一个来自系统创建者本人的第一手视角。