Lean 之父 de Moura 谈 Collatz 事件与 AI 时代形式化验证
Machine Learning Street Talk · rss · 2026-09-30
Machine Learning Street Talk 发布与 Leonardo de Moura（Lean 与 Z3 创造者）的长篇访谈，核心内容：
- Lean 的设计哲学：核心 kernel 保持极小并由独立检查器交叉验证，讨论了 Lean FRO 治理、Slack 清理事件与 Brandolini 定律。
- Collatz 漏洞事件：一个伪造的 Collatz 猜想"证明"同时被 Lean 官方 kernel 与 nanoda 独立检查器接受——原因是它利用了两者各自不同的 bug，引出"多 kernel 冗余、reward hacking 与透明性即安全"的讨论。
- AI 与形式化：涉及 Kim Morrison 用 Claude 完成 zlib 证明、AlphaProof 与 LLM 证明、为什么证书（certificate）仍然重要、规格变化下 AI 让重写证明更便宜，以及 agent 缺少的"面包屑式"学习能力和"有胜任力但无理解"的问题。
- Lean 4 与 Mathlib：依值类型的通俗解释、Lean 4 可扩展性、Mathlib 作为数学基础设施的现状与未来。
约 75 分钟，含完整时间戳与参考文献，另有 ReScript 转写与 PDF。
「漫话AGI」频道最新
- 开发者讽刺 CLI 智能体热:别再学思考读写了 — arthurcolle · 2026-09-30
- Greg Cook 论写作与思想：文字是静态能量，书写是传递的尝试 — GregCook2011 · 2026-09-30
- Plinz：AI 不是工具，而是「构建心智」的学科，数学才刚起步 — burny_tech · 2026-09-30
- 计算功能主义也难逃同一质疑：哪种计算才对应意识 — burny_tech · 2026-09-30
- 「大多数人只想要 slop」：技术圈误判普通用户对 AI 工具的需求 — max_paperclips · 2026-09-30
- “AI 取代一切”论遭群嘲:唱衰者往往从不接触该领域 — AndyMasley · 2026-09-30