机器核验之后，数学还需要谁来理解？Kevin Hartnett 谈 Lean 与 AI

一、嘉宾背景

Kevin Hartnett 是《Proof in the Code》的作者。书中追踪了开普勒猜想的计算机辅助证明，以及 Lean 创建者和合作者发展这套工具的过程。本集 Machine Learning Street Talk 由 Tim Scarfe 与联合主持人主持，全长五千六百一十三秒，约九十四分钟。除与 Hartnett 的讨论外，节目还收录了 Leo de Moura、Kevin Buzzard 和 Jeremy Avigad 等 Lean 参与者的讲述，将作者对历史的梳理与开发者、数学使用者对技术选择的解释放在一起。

Hartnett 对 Mathlib 的兴趣始于二〇二〇年为 Quanta Magazine 承担的一项报道任务。为写作本书，他反复采访六至七位核心消息来源，并查阅他们分享的邮件、公开的 Zulip 讨论，以及获分享的私人消息。这些材料使叙述得以深入项目的设计争论、协作过程和信任关系。

这些采访与记录构成了本集讨论的基础：Hartnett 关注数学工具及其社区如何改变证明实践，参与者的讲述则解释具体选择背后的考虑。从计算规模超出人工审查能力，到 AI 加快证明与代码生成，讨论始终追问同一组问题：谁来确认问题被准确表达，谁来维护知识的结构，以及机器完成核验之后，人是否获得了理解。

二、本期主要内容

开普勒猜想让计算机辅助证明面临的困难显现出来。节目开篇介绍，Hales 与 Ferguson 通过大量计算处理球体最密堆积问题，审稿人却难以确认这些计算如何共同构成完整证明。局部计算是否正确，与整套论证是否完备，需要不同层面的检查。de Moura 回忆，后续形式化工作使用了 HOL Light 与 Isabelle，将这套论证转化为可由机器核验的证明。

Hartnett 将日常数学中的信任描述为一个部分依靠社会关系的过程：人们依据已有知识、对作者的了解，以及对部分论证的仔细检查建立信心，通常不会逐行核验。de Moura 则指出，可检查的证明证书为协作提供了另一种基础，使从未见过面的人也能共同推进项目。贡献者之间的信任，不再完全依赖彼此的熟悉程度，也可以建立在提交结果能够接受统一检查之上。

Lean 既是编程语言，也是证明助手。它的检查内核负责核验证明是否符合推理规则。de Moura 强调内核应当足够小，并允许独立实现的检查器进行核验，因为一旦错误地接受假命题，后续推理也可能受到影响。在内核之外，可扩展的 tactics 作为辅助程序，自动完成重复的证明步骤，减轻逐项写出初等细节的负担。

这种表达能力伴随着实现和使用成本。Hartnett 将 Lean 的发展动机描述为获得比 Z3 更丰富的软件验证表达能力。Avigad 主张使用依赖类型论，以表达复杂的数学结构，同时也承认，这一选择会增加实现难度和使用负担。支持更广泛的数学表达，需要工具开发者承担相应的复杂性。

Mathlib 将这种表达能力积累为可复用的数学知识。Buzzard 回忆，自己在二〇一七年为库贡献了复数内容，随后招募本科生，将课程中的数学形式化。约三年后，库已覆盖他的本科生所学的大部分内容。推进到前沿数学时，他与合作者先梳理依赖关系、建立蓝图，再在 Lean 中给出完美空间的定义。这证明了 Lean 能够表达这一前沿对象，并不意味着与它相关的定理都已完成核验。

形式化也可以从不同规模的任务开始。Buzzard 介绍，Hales 曾建议先形式化定理陈述，再处理完整证明。他举例说，一篇论文中的素数 p 在前文已被限定为至少五；若脱离前文读取后面的定理，这个条件就容易被遗漏。另一项工作则深入到了关键推导：据 Buzzard 回忆，Scholze 在二〇二〇年十一月请求核验一段重要论证，此前读者曾略读其中约六页计算。团队找到的简化，将预计一年的工作缩短至约六个月，也带来了概念上的理解。明确陈述与完整证明各有价值，所需投入也不相同。

三、核心观点：推理、例子与边界

核验推导、忠实表达问题、增进理解，是三件需要分别判断的事。Hartnett 认为，数学贡献的价值还在于它能否带来可复用的概念和抽象。他以 Hales 的计算方法与 Wiles 的工作作对照，同时承认，难以解释的证明仍可能有用。机器证明能够解决一个问题，却未必同时提供探索后续问题所需的概念工具。

这也解释了形式化为何曾缺乏足够的吸引力。Hartnett 称，Hales 结果的形式化约耗费二十人年；节目还提到，形式化文本与非形式化文本的行数比可能达到二十比一，甚至更高。这些是讨论者对成本的描述，所供材料并未将其确立为普遍适用的测量结果。如果数学家原本就相信结论，为增加正确性保证而投入大量时间，未必比开展其他研究更有吸引力。改善概念组织、加深论证理解，则能为形式化提供另一种回报。

即使推导已经通过检查，信任仍有边界。节目所说的“形式化鸿沟”（formalization gap），是指核验一项推导，与确认其中的定义、假设和目标忠实表达了原问题之间的差距。检查器能够确认某个结论可以从给定定义和假设推出，却不能自动确认它就是人们原本想证明的命题。因此，哪些条件被写入、定义如何选取、形式陈述与自然语言是否对应，都需要另行审查。

一项定理陈述项目让这个问题具体起来。一位参与者称，团队对五十个《Annals of Mathematics》定理陈述进行了 AI 辅助检查，发现了转写错误，也发现了原文字面表述遗漏的条件，例如 n 至少为三、集合必须非空。这并不意味着原有数学成果被推翻：专家可能一直正确理解了隐含条件，只是字面陈述没有将其完整写出。这位参与者将补足条件形容为从百分之九十九走到百分之百；这一说法强调的是把隐含条件明确化，并非已经确立的论文正确率或 AI 可靠性统计。

形式化也可能通过概念组织增进理解。讨论者指出，为了让知识库的不同部分长期协作，数学家必须考虑信息如何封装、模块之间如何划分、通过什么接口连接。这些设计要求会促使人重新审视数学概念之间的关系。但能通过检查的表示，未必适合纳入公共知识库。Buzzard 强调，Mathlib 优先采用成熟概念，并选择适当的一般性；基础定义一旦改变，数千个文件都可能失效。AI 或许能够机械地修复依赖，却未必能选出更好的抽象。修复成本下降，并没有消除概念设计的必要性。

Hartnett 对自动形式化的观察，也指向同样的问题。他说，自动形式化能够比人工团队快得多地生成论文的 Lean 版本，但本集没有提供具体效率基准。产出加快，也给 Mathlib 的精确性、简洁性和贡献审查带来压力。通过核验只是其中一道要求；这些代码能否被复用、审查和维护，仍取决于它们采用的概念与组织方式。

AI 的数学成绩也需要区分其实现条件。据节目介绍，AlphaProof 在二〇二四年取得银牌水平的表现时，接收的是形式化题目，产出的是 Lean 证明，所用时间多于人类选手，并投入了大量算力。节目讨论的二〇二五年金牌水平结果则采用自然语言证明，评分安排也不同，那些竞赛答案没有经过 Lean 验证。Hartnett 还转述，DeepMind 在准备过程中，对代数与数论题的自动形式化约有八成达到近乎完美的程度；组合题因叙述性语言较多而更难处理。这是发言者引用的特定任务结果，不能据此推定任意数学文本的自动形式化成功率。

Tao 的 Equational Theories 协作项目展示了另一种数学探索方式。节目称，项目将约两千二百万个蕴含问题逐步缩减到剩余四个，并产生了 magma cohomology 等新构造。这里的价值既包括处理大量问题，也包括协作、计算结果与理论构造之间的相互推动。它展示了机器检查如何参与实验性的数学研究，但尚不足以说明所有数学问题都适合这一模式；问题数量的减少，也不能单独衡量理解是否加深。

四、学习与应用

对研究团队而言，首先需要明确每项形式化工作的成果范围：表达了什么对象，写明了哪些假设与结论，哪些推导已经通过检查。完美空间的定义、定理陈述的形式化，以及关键论证的核验，都可以构成独立而有价值的成果。区分这些成果，有助于在完整证明成本过高时继续推进，也能准确说明局部进展与整个理论之间的距离。审查时，应把原始意图与形式表达放在一起，确认检查器实际核验的内容。

定义审查可以借鉴 Commelin 与 Topaz 的做法：为重要定义构造具体例子，作为单元测试。这些例子能够检验定义在具体对象上的表现，为定义是否符合预期提供依据。但节目也强调，它们只能增加信心，不能决定性地证明定义已经捕捉到数学意图。例子通过之后，定义、假设与目标之间的对应关系仍需要审查。

软件团队同样需要检查规格究竟保证了什么。据节目介绍，Kim Morrison 的 Claude-agent Zlib 项目将 C 代码转写为 Lean，通过了原实现的测试套件，并证明任意数据在任意压缩级别下，经过压缩与解压都能恢复原样。所供材料没有包含实现或证明文件，因而无法据此独立核查这些结果。讨论者随后指出，如果压缩和解压都只是原样返回输入的恒等函数，也能满足往返恢复。这说明，一项性质即使得到证明，仍可能不足以表达软件的预期功能。

节目提出，可以考虑增加输出大小或与原实现比较的性质。这些是补充规格的建议，并非项目已经确立的结果，也不能由此推出所有输入压缩后都应变小。应用这些建议时，需要明确适用输入、比较条件和预期行为，并分别说明测试覆盖了什么、形式证明覆盖了什么，以及哪些需求尚未写入规格。一项有用的保证，只有在范围清楚时，才能为软件是否满足目标提供可靠依据。

人类审阅代码的 AI 辅助开发，与完全不检查代码的自主开发，对规格完整性的依赖程度也不同。节目指出，人仍在阅读代码时，可以结合开发目的发现规格之外的问题；不再检查代码之后，这部分判断就更依赖规格是否覆盖预期行为。因此，扩大自主开发范围时，需要同步审查输入输出、关键性质与实际目标之间的关系。AI 可以参与编写规格，但生成的规格本身也需要接受审查。

公共库的自动化收益，还应计入审查与理解的成本。Buzzard 关于基础定义可能影响数千个文件的提醒，以及 Hartnett 对自动形式化给 Mathlib 带来压力的观察，都表明，通过检查的代码仍需要合适的概念、依赖关系和可复用接口。主持人将审查债务、验证债务和理解债务列为智能体编程的障碍；回应者提出用 AI 辅助编写规格，并将 Harmonic 从数学证明走向软件验证的策略描述为一项结果尚不确定的押注。这些方向值得通过范围明确的成果逐步检验，同时持续审查目标、规格和维护要求。

来源

• 原始节目：Mathematics Just Changed Forever — Kevin Hartnett