Kevin Hartnett：Lean、数学证明与 AI 验证的边界

记者 Kevin Hartnett 与 Tim Scarfe 一起讲述 Lean 的发展历程、创建它的人，以及证明在数学中不断变化的作用。参与讨论的数学家和计算机科学家都希望提高数学推理的可靠性，但对形式化验证能带来什么并不完全一致。

故事从开普勒猜想开始：相同大小的球体能以多高的密度堆积？Thomas Hales 和 Samuel Ferguson 给出的证明依赖大量计算。审查这一证明给数学家带来了格外沉重的负担：他们既要评估漫长的论证，也要检查实际上无法由人手逐项核验的计算。

主持人介绍说，Hales 和 Ferguson 将球体堆积问题化简为大量不同情形，再结合数学推理与计算机运算，为每种情形的密度建立上界。正是这一证明的规模，让完整审查如此困难。

Hales 把成果送交《数学年刊》时，编辑遇到了一个陌生的审稿难题。审稿人可以检查单独的部分并认为它们可信，但整个论证包含大量计算和计算机代码；要弄清所有部分如何共同支撑结论，又是另一回事。

随着审稿迟迟不能结束，Hales 重新考虑了将相同方法用于其他问题的计划。如果数学家难以验证他现有的结果，那么在其他地方使用同样庞大的计算，可能产生更多无法让学界放心接纳的成果。形式化验证正是从这种实际的信任问题中发展起来的。

De Moura 把之后的形式化工作称为 Lean 出现之前的一个里程碑。Hales 使用已有的证明助手，表明数学界关心的重要定理可以借助这类工具检验。Hales 后来选择用 Lean 开展其他工作，也提高了 Lean 的知名度。

数学证明历来既依赖逻辑论证，也依赖一个社会过程：研究者写出证明，其他专家进行研究，人们通过审阅和使用逐渐建立信心。这个过程很有力量，但受访者指出，证明日益漫长、复杂，也可能让独立检查变得困难。

De Moura 认为，可检查的证明证书有助于互不相识的人协作。大型项目可以拆成较小的命题，不同经验水平的参与者都能贡献成果。项目组织者仍然需要关心，最终工作是否容易理解和维护。

正确性并非数学家对证明的唯一要求。一个证明可以确立结论从假设中成立，却不一定让读者获得使结果豁然开朗的概念性洞见。形式化检查解决了其中一部分问题；理解论证为什么有效，仍是另一个问题。

Hartnett 区分了回答一个问题与发展能开辟新领域的方法。即使计算证明不像更抽象的论证那样提供同样的概念工具，它仍然可以是有效的。Paul Lessard 则强调，人需要能够理解的解释：得到答案和弄明白答案为什么正确，是不同的目标。

形式化需要时间。Hartnett 说，开普勒猜想的形式化工作大约投入了二十人年，形式化代码与非形式化数学文字的比例也可能很高。对于已经相信某个熟悉结果的数学家来说，仅为检查它而投入这么多时间，可能不如追求新的发现有吸引力。

Lean 既是一门编程语言，也是一种交互式定理证明器。使用者用精确的语言表达定义、命题和论证，再由 Lean 检查证明是否符合所声明的命题。它并不是简单地读入一篇普通数学论文，就能判断其论证是否成立。

较小的内核有助于界定系统中必须信任的部分。De Moura 解释说，接受一个无效证明比拒绝一个有效证明更严重：后者会阻碍工作，前者却可能让错误结果成为后续结论的依据。小型检查器也更容易让其他人独立实现。

Leonardo de Moura 此前开发过 Z3 求解器，希望有工具帮助人们推理软件的正确性。Lean 正是在这种兴趣中发展起来的。证明程序具有某一特定性质，与证明程序不存在任何错误，是不同的事；保障的范围取决于实际声明并检查了什么。

Z3 的成功也让 de Moura 看到了自动定理证明的局限。自动求解器在能够处理的问题类别中很强大，但他希望获得一种表达能力更丰富的语言，让人可以引导论证的构造。Lean 的交互式方法使使用者能更主动地参与组织证明。

Hartnett 将这本书描述为一个工具的发展故事：它最初受到软件验证的推动，后来被数学家用于自己的研究目的。这种转变并非自动发生；社区需要建立数学库，并处理软件验证、数学研究和教学之间的不同需求。

Jeremy Avigad 介绍了数学表达背后的一项设计选择。Lean 使用依赖类型论，让定义和证明能够在结构丰富的语言中表达。这类基础提供了组织推理的有用方式，但其好处也必须与学习、实现和维护系统的复杂度相权衡。

De Moura 最初更倾向于一种简单的逻辑基础，认为它更容易实现，也足以应对许多验证任务。Avigad 则认为，依赖类型论更适合现代数学中的代数结构网络。不同的人基于使用证明助手的经验，共同商讨了这一选择。

Avigad 曾使用 Isabelle 和 Rocq。他称赞 Isabelle 的自动化能力，同时解释说，某些抽象代数内容更容易用表达能力更强的类型系统表示。这种表达能力也有代价：依赖类型论更难实现，并给使用者和开发者带来更多边界情况。

2013 年，de Moura 决定让 Lean 采用依赖类型论。后来他看到，数学库中的抽象概念甚至对密码学等软件验证任务也有帮助。按照他的说法，早期增加的工作最终有了回报，因为系统既能服务数学家，也能服务证明程序性质的人。

Hartnett 说，de Moura 当时是一名没有大型工程团队的研究者，却要回应不断增加的使用者。数学家喜欢这个工具，也不断提出功能需求；de Moura 希望帮助他们，但支持工作占用了他实现长期设想所需的时间。这些相互竞争的需求成为挫折的来源。

数学家 Kevin Buzzard 思考过，要确切知道文献中哪些结果已经完全确立，有时会非常困难，随后他对 Lean 产生了兴趣。他担心的不是数学普遍没有价值，而是已发表论文可能省略细节，而检查这些缺口需要大量人力。

Buzzard 刚接触证明助手时，其中形式化的大多是基础内容。如果目标是检查前沿研究，这可能令人失望，但他也发现这一过程很有趣。问题不再只是机器能否发现错误，还有一个社区能教会软件表达多少数学知识。

他对缺口的担忧，针对的是建立在快速发展的领域之上的论文，并非说 Scholze 自己的基础工作不严谨。Buzzard 希望将论证转化为形式语言，在必要时找出缺失的细节，建立后续研究可以依赖它们的信心。

这个库就是 mathlib：由 Lean 使用者协作建立的定义和定理集合。贡献者不只是把孤立的证明放进去，还必须决定怎样表达概念，才能让不同领域的成果彼此配合，并供后来者继续构建。

Hartnett 把 mathlib 的建设比作大家共同搭建谷仓。贡献者从基础开始建立定义和结果，供其他人使用。证明助手也许拥有逻辑规则，但没有这样的库，每位使用者都得为严肃项目重新建立大量数学背景。

Buzzard 回忆了自己贡献复数相关内容、让学生参与形式化的经历。数学家眼中看似平常的背景知识，必须描述得足够精确，检查器才能处理。这个过程可能揭示论文没有显示出的选择，也让新人有具体途径参与共同的数学项目。

Buzzard 组织学生贡献他们在本科阶段学习的内容。他几乎把数学库当作一个学生：先教定义，证明基本事实，再进入下一个主题。世界各地也有其他团队做同样的事，知识由此积累成共享基础设施。

维护者还必须判断，一个想法何时足够成熟，适合进入这套基础设施。Buzzard 说，有前途的前沿概念可能仍在变化，而共享库更需要得到充分理解、抽象程度恰当且有用的定义。以后修改基础定义，可能导致数千个依赖文件失效。

Buzzard 最初帮助形式化了概形，以向数学家展示 Lean 能够表达复杂几何。后来有同事认为概形早已不是前沿数学，团队便选择了更新的目标：Scholze 的完美域空间。Buzzard、Patrick Massot 和 Johan Commelin 列出了实现目标所需的中间定义。

Hartnett 说，形成的数学库有着广阔的基础，同时有少数狭窄的高塔伸向研究前沿。成功形式化一个高级定义，并不意味着周边每个领域都已建好；但它表明，基本语言和足够的支撑材料能够表达复杂的现代数学对象。

Buzzard 回忆自己看过 Hales 关于现代数学形式化的直播演讲。Hales 建议先从定理的陈述入手，而不是要求每位数学家编码完整证明。写出精确陈述的任务较小，同时仍能让读者清楚知道作者声称证明了什么。

Buzzard 举了一个例子：论文前面某节声明素数 p 至少为五，后面某个定理又使用 p。从后面开始读的人可能漏掉这个限制。将陈述明确编码，会迫使作者判断哪些假设属于定理的一部分。

即使建立在定义之上的定理需要漫长证明，定义本身也可能相对简短。对 Buzzard 来说，这让 Hales 的提议成为基础数学库与研究论文之间可行的桥梁。他后来获得支持，开展翻译近期定理陈述的项目；据他说，访谈时工作约完成了五分之一。

Hartnett 解释了为什么这项工作有时出乎意料地繁琐：人认为显而易见的步骤，仍然必须从定义和既有事实中推导出来。困难不在于数学家怀疑简单算术，而在于计算机需要可以检查的中间论证。

Lean 的 tactics 可以自动处理常见推理模式。使用者无需手工提供每一个常规算术步骤，而可以调用辅助程序来构造必要的证明。De Moura 编写了一些 tactics，也让社区成员能够自行编写，从而减少重复劳动，同时保留内核的检查作用。

2020 年，Scholze 就近期一篇预印本中的特定定理联系 Buzzard。Buzzard 曾参加阅读该论文的学习小组，但回头检查时发现，小组只是粗略浏览了那段六页长的技术计算。Scholze 询问过的其他专家给出了类似回答。

Scholze 认为，已有数学库中的知识或许足以表达其中许多内容。Buzzard 看到一个用 Lean 检验最新研究成果的机会，尽管当时社区规模很小，证明也很复杂。经 Scholze 同意，他公开了挑战，吸引了一些愿意投入大量时间的人。

团队仔细阅读证明时，Commelin 找到一种简化方法，缩短了工作。六个月后，团队检查完核心命题。Buzzard 说，结果让 Scholze 放心，也为证明的一部分提供了更具概念性的论证：形式化既帮助人们检查数学，也帮助人们理解它。

项目的关注度吸引了更多数学家使用 Lean。一位专家可能问数学库能否立即处理自己最新的定理，却发现该领域的基本对象还需要先建立。不过，这些交流仍帮助社区将数学库扩展到更多领域。

Hartnett 指出形式化证明的另一个好处：读者可以检查各部分如何相连，而不用把文章仅仅看作一串静态陈述。证明助手可以明确显示依赖关系，让读者从一个命题追溯到它所依赖的内容。

参与者询问，从数学公理出发的 AI 是否会重新发现人类选择发展的数学领域。Hartnett 转述了一些数学家的猜测：这样的系统可能很早就与人类的发展路径分道扬镳。人类偏爱感觉有意义、有用的定义和抽象，而只以有效陈述为目标的搜索不一定有相同偏好。

数学问题对强化学习也有吸引力，因为正确解答可以提供相对清晰的反馈信号。Hartnett 将国际数学奥林匹克竞赛描述为一个具有挑战性的目标：题目使用中学阶段的知识，却要求异常精妙的推理。

在 2024 年奥林匹克竞赛中，DeepMind 使用 AlphaProof 处理形式化的问题，并生成 Lean 证明供检查。DeepMind 多个系统的综合表现达到银牌水平，但它们获得的时间比人类选手多，也使用了大量计算资源。Lean 检查也为 AlphaProof 的训练提供了反馈。

AlphaProof 不能像普通读者那样直接读懂每道竞赛题。把自然语言问题转换为形式化陈述，本身就是另一项挑战。方程让一些代数和数论题更容易形式化，而以故事形式表达的组合数学问题更难翻译。

在 Equational Theories 项目中，Terence Tao 组织大规模协作，梳理代数定律之间的蕴含关系，并用 Lean 检查结果。参与者把约二千二百万个问题缩减到几百个，最后只剩少数顽固的问题。项目的意义不止于填完表格，还在于尝试协作、探索式的数学研究方式。

Tao 将这项工作比作物理学中的实验研究。大规模计算和协作可以发现值得研究的结构，而不必取代理论。参与者说，他们在过程中发现了意想不到的构造，说明探索陌生领域可以提出原先目标之外的问题。

2025 年，DeepMind 和 OpenAI 还报告使用自然语言证明取得奥林匹克竞赛金牌水平的结果，这些答案并非依靠 Lean 验证。Hartnett 预计两种方式都会发挥作用：形式化环境可以提供训练反馈、帮助筛选大量尝试，而自然语言系统也可能有助于给出数学家能够评估的解释。

Buzzard 看到了快速形式化与 mathlib 设计原则之间的张力。维护者希望找到能让后续工作更容易的抽象；AI 系统却可以一路推进，生成漫长、笨拙但能通过检查的翻译，不一定停下来思考底层定义是否以最有用的方式组织。

新工具也能帮助维护。Buzzard 想象，基础定义改变后，AI 可以修改大量依赖它的证明。但他认为，自动修复机制的存在，并没有消除数学库对概念清晰性的要求：维护者仍要决定什么内容应该被接纳，以及它如何与其他部分配合。

Hartnett 指出，AI 可以降低 Lean 语法的使用门槛，可能让更多数学家使用该系统。自动形式化也带来了更快翻译论文和教材内容的可能。但大量涌现的代码也把工作转移给负责检查质量、将其整合进连贯数学库的人。

证明检查器回答的是：一个推导是否建立了给定的形式化陈述。它本身不能保证该陈述准确表达了数学家的意思。如果 AI 形式化了错误目标，或者遗漏了预期条件，即使 Lean 证明完全有效，人类的问题仍可能没有得到回答。

Buzzard 认为，普通数学文字并不总像它的声誉所暗示的那样明确。专家常常会根据上下文理解没有写出的假设。将陈述翻译成形式语言时，翻译者必须决定是逐字编码纸面上的内容，还是补上读者通常会推知的条件。

他介绍了一个形式化《数学年刊》上五十个定理陈述的项目。据他所述，AI 审查既发现了翻译过程中引入的错误，也发现某些已发表的表述遗漏了专家会认为显而易见的假设。这个例子关乎命题表述的精确度，并不是说底层数学思想普遍错误。

Avigad 回忆，早期主要以发现错误为理由推广证明助手，并没有说服许多数学家。数学家最关心的是思想与理解。严谨是表达和检查思想的媒介，但一串经过机械验证的步骤，本身不等于使证明有价值的洞见。

不过，形式化也能带来新的理解。Avigad 把建立数学库比作设计软件接口：人们必须选择一个定义公开哪些内容、不同模块如何配合，以及它们交互需要哪些假设。在这些约束下重新审视熟悉的数学，可以让人以新方式看到它的结构。

Liquid Tensor 的工作也暴露了一个类似的定义问题。Scholze 担心 Lean 能够验证关于某个形式化对象的论证，而该形式化定义却没有捕捉到数学家真正想表达的对象。一个定义不能仅因语法正确就被认为合适；人们必须判断它是否符合自己的目的。

Commelin 和合作者的一部分回应，是为重要定义编写具体例子，类似单元测试。例子无法证明一个定义涵盖所有预期特征，但可以显示它在熟悉的情形下是否按预期表现。讨论把测试视为数学判断之外增加信心的一种方式，而不是判断的替代品。

De Moura 还谈到了维护共享项目的人力成本。提出想法可能很容易，评估却很昂贵：维护者发现缺陷，提出者修改想法，后续每次审查都要花更多时间。系统不断扩大时，这种不对称使专注和审慎审查成为重要资源。

zlib 压缩格式的一份 Lean 实现同时展示了 AI 辅助的潜力和规格说明的局限。讨论描述了翻译实现、运行测试，并证明一条往返性质：解压缩压缩后的数据，可以得到原始输入。这是一条有用的性质，但只是所需系统的众多性质之一。

De Moura 给出了不完整规格说明的简单反例。如果唯一要求是压缩再解压后返回输入，那么两个函数都可以原样返回输入。所述性质仍然成立，但数据根本没有被压缩。增加测试和性质，能够缩小已检查内容与用户实际需求之间的差距。

这种差距对 AI 生成的软件尤其重要，因为编写完整规格说明本身可能很难。参与者讨论了 AI 能否既帮助写代码，也帮助写规格说明，以及验证能否缓解生成程序日益严重的审查瓶颈。Hartnett 将其描述为正在进行的尝试，而非已得到证明的解决方案。

Buzzard 乐观地认为，AI 和形式化工具将加速数学研究，发现更多定理，并开辟陌生领域供人探索。其他数学家则因学科变化而感到担忧或悲伤。讨论没有假定所有人追求相同结果，而是承认变化的速度与后果仍不确定。

Avigad 把人的问题放在中心：人们有什么目标，又该如何使用这些系统实现目标？对他来说，一台自行证明结果的服务器，不如人们如何与它互动、通过互动获得什么理解更值得关注。

Hartnett 说，采访写书的过程让他感到，自己对那些毕生工作被写入故事的人负有伦理责任。他多次采访关键人物，利用大量电子邮件和 Zulip 讨论记录，重建软件背后的决定与关系，而不是把 Lean 写成一个一出现就已成熟的工具。

他发现，曾有一段关系紧张的时期，使 de Moura 开发 Lean 4 的工作与继续建设 mathlib 的部分数学社区分离。不同的愿景和鲜明的个性都促成了摩擦。参与者描述的是一个关系紧密、同时存在真实分歧的社区，而不是能够简化成英雄与反派的故事。

Avigad 回忆了在西雅图与 de Moura 重新联系的经历：两人从会议和工作中抽出时间，一起散步，既聊 Lean，也聊其他事情。回望早期经历，他说项目的发展令人感到恍如隔世。Scarfe 最后推荐读者了解 Hartnett 对这些人物和坚持的记录。