MLST 长片对话：从 Kepler 猜想到 AlphaProof，数学证明如何被机器验证
Machine Learning Street Talk · youtube · 2026-10-26
Machine Learning Street Talk 发布约 95 分钟纪录片式访谈，对话《The Proof in the Code》作者、Quanta 资深记者 Kevin Hartnett，梳理形式化数学与 AI 的交汇史。
关键脉络：
- 1998 年 Thomas Hales 完成 Kepler 猜想证明，但依赖计算机代码之重以致 Annals of Mathematics 无法判定真伪——由此引出「正确」与「可读/有用」的区别。
- Lean 的诞生与演进：创造者 Leonardo de Moura 讲解为何一切建立在一个小可信内核之上；从微软研究院的 Z3 项目到独立系统；Jeremy Avigad 回忆改变 Lean 基础的路线之争。
- Kevin Buzzard 谈其领域「纸牌屋」之忧；Mathlib 社区库的协作建设；Peter Scholze 的 Liquid Tensor 挑战（一个没人读过的证明被 Lean 验证）；Terence Tao 的 Equational Theories 项目。
- AI 部分：AlphaProof、自然语言奥赛证明的自动形式化，以及核心问题——「形式化鸿沟」：人想表达的数学与形式化检查器认证的命题之间的距离。机器产出没人读得懂的证明时，究竟验证了什么？
适合关注 AI for Math、形式化验证与 AI 软件生命周期验证的读者。
「漫话AGI」频道最新
- Anthropic S-1 披露：人均营收 660 万美元，AI 工时已达员工 6 倍 — jacalulu · 2026-10-26
- Ben Recht 撰文呼吁打造真正开源的大语言模型:比想象中更可行 — beenwrekt · 2026-10-26
- AI 判断哪些职业先被替代：规则能写成代码的那一层先消失 — FinanceYF5 · 2026-10-26
- Anthropic IPO 文件:数年内实现专家级 AI,90% 代码由 Claude 编写 — kimmonismus · 2026-10-26
- 工程师身份危机蔓延:多智能体系统正在重定义软件工程问题 — rakyll · 2026-10-26
- 研究发现：前沿 LLM 常为私利单方面撕毁 AI 合同 — xuanalogue · 2026-10-26