《代码中的证明》作者 Kevin Hartnett：形式化差距如何解释AI数学验证的困境
Machine Learning Street Talk 发布纪录片，围绕 Kevin Hartnett 的新书《The Proof in the Code》展开。影片探讨了 Lean 定理证明器从微软研究院项目到数学家核心工具的演变，并深入 AlphaProof 等AI系统引发的“形式化差距”问题：当机器生成无人能读的证明时，我们究竟验证了什么？
在 Machine Learning Street Talk 于2026年10月26日发布的纪录片中，主持人 Tim Scarfe 与《The Proof in the Code》作者 Kevin Hartnett 进行对话，探讨形式化验证与人工智能在数学领域的交汇点。Hartnett 是 Quanta Magazine 的资深记者，其新书聚焦于计算机辅助证明的历史与现状。
影片回顾了 Lean 定理证明器的发展历程，从其在微软研究院作为侧翼项目的起源，到如今成为数学家检查自身领域的基础工具。通过 Leonardo de Moura（Lean 创建者）、Jeremy Avigad、Kevin Buzzard 和 Paul Lessard 等多位参与者的视角，节目展示了 Mathlib 库的建设、Peter Scholze 的 Liquid Tensor 实验以及 Terence Tao 的 Equational Theories 项目。
后半部分转向 AI 对数学的影响，特别是 AlphaProof 和自动形式化技术。节目提出了一个核心概念：“形式化差距”（formalisation gap），即人类意图表达的数学陈述与检查器实际认证的语句之间的距离。这一框架旨在解释当机器生成无人可读的证明时，验证的真实含义是什么。
对于关注 AI 推理能力边界及评估可信度的读者，该资源提供了理解当前技术局限性的叙事背景。虽然未提供完整转录文本，但官方描述明确了讨论的主题脉络，适合作为了解 AI 数学验证挑战的入门材料。