一个“吹毛求疵”的学生，正在改变数学证明

luyuanhong

一个“吹毛求疵”的学生，正在改变数学证明

数学证明建立在公理之上，追求绝对的逻辑严密。然而，哪怕是最伟大的数学家，耗费数年所得的成果也可能因一个细微的疏漏而崩塌。面对人工校验困难，错误难以避免的现实，“证明助手”应运而生——以机器审视每一步推导，确保证明无懈可击。而今，随着 AI 的加入，形式化证明正迈向新的阶段。也许，希尔伯特那场“让数学彻底形式化”的梦，正悄然接近实现。

撰文 | Ben Watkins

翻译 | Logic Moriaty

审校 | 7 号机

人类数学家难免出错。证明助手应运而生，助其查漏补缺，而在这个过程中，它们也将数学转化成了一种高度合作的体验。

什么是证明？

数学只是一种依照特定简单规则，在纸上操作无意义符号的游戏。

——大卫·希尔伯特（David Hilbert）

这话听起来有些悲观。

数学不同于科学。尽管二者之间互动密切（有些人认为数学是科学的语言），但它们是完全不同的两种游戏。科学本质上是一种基于观察与经验的游戏；在科学中，只有那些在我们观察到的世界和宇宙中显现出来的事物，才被视为真实。而数学则是一种基于公理的游戏。

公理可以看作是数学的规则。它们是无法从其他东西推导或证明出来的基础，我们在此基础上构建起整个数学体系。皮亚诺公理（Peano axioms）便是公理集合的一个范例，它是自然数的公理体系。其中包括一些像“0 是一个自然数”、“若 x=y ，则 y=x ”这样的陈述。在某种意义上，它们是“显而易见”的陈述，或是用希尔伯特的话来说，它们是“简单的规则”。在数学中，断言某个命题为真，例如“存在无穷多个素数”，就意味着我们可以证明这个命题能够归结于这些公理。数学中所有的美妙之处，所有复杂精妙的结构和简洁强大的定理（或者说是某些人眼中的“纸上无意义的符号”），在某种意义上，都不过是从公理中幸运衍生出的产物。

话虽如此，但这并不是做数学的真实体验。几乎所有的纯数学论文都不会提到公理。相反，在实际的研究体验中，更多是通过将待证明的定理归结于先前已经被证明的命题来完成证明。不妨在脑海中勾勒这样一幅图景：一棵枝繁叶茂的大树，基础定理如同主枝一样从公理的树干上生长出来，较小的枝条从主枝延伸而出，更细的嫩枝又从这些小枝上萌发。最终，每条嫩枝都能追溯回树干，但是实际上，将其视作所属枝条的延伸往往更为实用。（当然，这个比喻的局限性也是显而易见的。比如某些定理存在多种证明路径，或者有些命题虽然成立却暂无证明，此时这样的比喻就显得比较牵强。）



然而，至关重要的是，必须确保论文中的证明是正确和完整的。

一个例子：四色定理

四色定理（Four-colour theorem）说的是，任何有边界的地图（例如美国地图）都只需使用四种颜色来着色，就能使得任何共享边界的两个区域颜色都不相同。

您可以给一百万张地图着色，来尝试验证四色定理，但是这并不能算是一个证明。万一存在您尚未发现的反例呢？在 1879 年，阿尔弗雷德·肯普（Alfred Kempe）似乎认为他已经证明了反例不存在，并发表了对该定理的“证明”。然而 11 年后，珀西·约翰·希伍德（Percy John Heawood）证明了这个“证明”实际上是错误的——肯普的证明中使用了一个错误的假设。

这便引出了一个很自然的问题：当一个证明发表时，我们应该如何确定它是正确的？如何确保它是数学之树上的一条新枝，而非一条注定孤独坠地的枯枝？肯定存在某种方法可以检查这些证明是否正确的，对吧？

同行评审通常就是解决这个问题的方法。也就是说，当一篇论文发表时，一小群其他的数学家会检查你的工作。然而，假如这些同行也没发现你的错误怎么办？更何况，如今动辄数百页的长篇论文屡见不鲜。所以实际上，单凭人力根本无力全面检查。

这便催生了对于“证明助手”（proof assistants）的需求。 证明助手是由计算机科学家开发的软件工具，通过要求每一步推导都以形式化语言表述，来验证一个证明是否正确。如若未能满足要求，程序便会判定该证明不完整。

凯文·巴扎德（Kevin Buzzard）是伦敦帝国理工学院的纯数学教授。在巴扎德参加艾萨克·牛顿研究所的“大证明计划”（Big Proof programme）完后，笔者曾与他见面（文章稍后会详细介绍！）。他解释道：“嗯，事情是这样的，如果你在和一个象棋计算机对弈，那你根本无法走出违反游戏规则的一步，对吧？在象棋中，很容易识别对方是否走了违规的棋步，但是在数学中却不是这样，数学比象棋要复杂得多。我们会看到一些发表的论文有错误，虽然很少见，且错误往往无关紧要，但有时候会出现非常大的错误。而使用证明助手做数学研究，一定程度上消除了出错的可能性……整个数学体系在没有它们的情况下当然也能照常工作，但现在已经是 2025 年了，我们完全可以拥有这点额外的保障。只要我们想要，我们就可以获得这个额外的优势。”

例如，四色定理的第一个正确证明是由肯尼斯·阿佩尔（Kenneth Appel）和沃尔夫冈·哈肯（Wolfgang Haken）于 1976 年给出的。他们通过将需要验证的可能反例的数量从无穷多（相当庞大的一个数量）减少到 1,834 个（依然很多，但是已大幅减少）来完成这一证明。随后，他们借助计算机验证了这些情形均不构成反例。完整的证明发表，并附有超过 400 页的微缩胶片补充材料。其篇幅之长，对于任何（心智正常的）人来说，根本不可能逐一检查。

然而到了 2005 年，本杰明·维尔纳（Benjamin Werner）和乔治斯·冈蒂尔（Georges Gonthier）在证明助手  Rocq（前身为 Coq）中给出了一个完全形式化的证明。

证明助手究竟是什么？

凯文·巴扎德将证明助手形容为一个特别学究式（过分严谨）的学生。想象一下，你正在讲台上讲课，尝试证明某个结果。每当你在证明中做出任何一步，哪怕是像在方程两边加 1 这样显而易见的步骤，坐在教室前排的一个特别让人恼火的本科生总会举手发问：“这个为什么成立？”

当你使用证明助手时，你将需要编写一些代码，而代码只有在所有细节都得到明确阐明的前提下才能运行。假设你在进行某个证明的时候，需要使用某个定理，而这个定理有三个前提条件。也就是说，这个定理表示，如果你已知关于某个特定对象的三个属性（例如，它是一个自然数，它大于 3 ，它是一个质数），然后你就会知道一些关于它的结论（例如，它的平方可表示为 24 的倍数加 1 ）。那么，当你使用这个定理时（例如，对像 43 这样的数字），除非你证明它满足所有前提条件（即，它是自然数，它大于 3 ，并且它是质数），否则代码无法运行。

这种如同“杠精”一样的过分严谨在做数学时并不常见，但它却可以使我们放心，当代码能够运行时，证明肯定是正确的。下面的部分将进一步介绍如何使用证明助手证明其他的复杂定理，以及它们如何改变人们研究数学的方式。

证明助手：创作社群

在本文前面的部分中，我们探讨了什么是证明助手。当然，人们对证明助手的期望，是希望它能够检验比上一节示例更为复杂的数学证明。2023 年 11 月，一项名为多项式 Freiman-Ruzsa 猜想（Polynomial Freiman-Ruzsa conjecture）的数学定理得到了证明。证明这个源自组合数学领域的著名猜想是一项非常艰巨的任务，但最终由一个杰出的团队完成：蒂莫西·高尔斯（Timothy Gowers）、本·格林（Ben Green）、弗雷迪·曼纳斯（Freddie Manners）和陶哲轩（Terence Tao）。


陶哲轩

这个猜想的证明是一篇 33 页，基本自成一体的论文（也就是说，论文中的证明并没有过多依赖其他论文的已有成果）。特别是，这篇论文看起来是那种非常适合尝试通过像 Lean（Lean 是微软研究院在 2013 年推出的计算机定理证明器，同时也是一门通用函数式编程语言）这样的证明助手来验证的类型。因此，由陶哲轩牵头，大约三十名研究者组成的团队，集思广益，致力于将这一证明形式化。

值得注意的是，尽管这是组合数学领域的一项成果，但并非所有的参与者都是组合数学家。他们甚至不全是数学家；其中一些是计算机科学家，还有一些仅仅是享受解谜乐趣的人。在证明形式化的初始阶段，会先搭建一个证明框架，从而将整个“谜题”分解成许多部分。这种框架被称为依赖图（dependency graph）。


形式化证明多项式 Freiman-Ruzsa 猜想过程中期的依赖图示例。图片来源于陶哲轩的博客

这是多项式 Freiman-Ruzsa 猜想在证明形式化过程中期的依赖图示例。图中每个气泡要么代表一个定义（矩形），要么代表一个定理/引理（椭圆形）。可以看到有箭头指向不同的形状。当某个定理/定义被其他定理/定义需要时，箭头便会从前者指向后者。随着时间的推移，所有参与者的贡献会让图表逐渐变绿（这意味着特定的定义或引理已经完成了编码和检查）。当定理被完全形式化时，整张图表将变成令人满意的深绿色，最终甚至能给人们带来大量的多巴胺快感。对于多项式 Freiman-Ruzsa 猜想，这一过程耗时约三周。您可以很容易地将其类比为我们之前的大树比喻。我们想要接上最终的那根枝条（多项式 Freiman-Ruzsa 猜想），但必须从箭头所指的那几个分支开始。

数学这门学科，素来享有"孤军奋战的学科"之名，而这一印象在历史上不无依据。下图通过十个数学领域的聚类分析，展示了各领域论文的平均作者数量。


十个数学领域聚类中单篇论文的平均作者数量。Gen：普通数学/历史/基础，Disc：离散数学/凸几何，NTAG：数论/代数/代数几何/群论，Ana：实分析与复分析，OpTh：调和分析和泛函分析/算子理论，DIEq：微分方程和积分方程，OptCS：最优化/数值分析/计算机科学/算法，ProbStat：概率论与统计学/经济学、生物学应用和医学，TopGeom：拓扑与几何，MaPh：数学物理。

诚然，参与单篇论文研究的数学家数量确实呈增长趋势。但是即便如此，能有二十人左右共同参与的数学项目，至今依然十分罕见。

除了与其他人共同参与的乐趣外，这种协作模式的优势在于，对于那些规模更大、可能也更复杂的证明，它能让不同研究者根据自己的个人兴趣与专业背景，各自投身于证明形式化过程中最契合自身的环节。

费马大定理


凯文·巴扎德，由托马斯·安格斯（Thomas Angus）拍摄

以著名的费马大定理（Fermat's last theorem）为例，该定理于 1994 年由安德鲁·怀尔斯（Andrew Wiles）在理查德·泰勒（Richard Taylor）的帮助下成功证明，举世闻名。2024 年，英国工程与物理科学研究委员会（Engineering and Physical Sciences Research Council，EPSRC）拨付了一项五年期资助，支持凯文·巴扎德在 Lean 上完成该定理的形式化证明。

他的最初目标是将费马大定理简化为 20 世纪 80 年代就已知的成果。但是怀尔斯的证明非常复杂，涉及群论、交换代数、实分析、复分析、代数几何、微分几何等多个数学领域的工作。巴扎德坦言自己并非实分析的拥趸：“如果我倾尽余生去做这个工作，到死我可能都还在做实分析。”然而，随着项目人数的增加，这意味着可能更偏爱证明某个领域（比如实分析）的合作者可以专心做那部分工作，没有人需要了解整个证明是如何运作的。


这是费马大定理立方情形（即两个立方数之和不可能等于另一个立方数）的依赖图。该图取自皮特罗·蒙蒂科内（Pietro Monticone）关于费马大定理形式化项目的网站。

机器学“形”

如果我们能够将形式化证明助手与大语言模型（large language models ，LLMs）如 ChatGPT 、DeepSeek 、Gemini 或 Llama 结合使用，这将释放出巨大潜力。这些人工智能模型在数学方面确实已经变得相当出色。最近（2025 年），更有大语言模型在国际数学奥林匹克竞赛中达到了金牌标准。

然而，它们并不完美，目前最大的问题之一无疑就是 “幻觉”，即大语言模型会犯错误。凯文·巴扎德解释道：“关键问题在于，它们该如何改进？……目前人们认为存在两种不同的技术路线，对吧？有些人认为我们应该继续做我们正在做的事，减少模型幻觉，投喂更多数据，最终让它们读完这间办公室里所有论文后就能变得更加出色。但我的建议实际上是，不，我们应该教会它们形式化语言，从根本上让它们不再产生幻觉。所以，谁知道哪条路会胜出……我赌形式化语言这一边。”

目前大语言模型还存在一个问题是，当遇到瓶颈时，它们的本能不是像人类那样放弃，而是选择撒谎或者编造证明。绕开这个问题的一种方法是，要求大语言模型生成符合 Lean 规范的代码。也就是说，它们必须先用 Lean 写出证明，而不是直接生成供人类阅读的证明文本。然后运行 Lean 代码，它会告诉模型证明哪里不正确，或者是否存在漏洞。这样，大语言模型就必须检查自己的错误，而不是用那些可能蒙混过关的含糊表述来逃避检验。

当然，在此之后，它们完全可以将 Lean 代码转译回自然语言。若想要让大语言模型真正能够开始做研究级数学（如果它们能够做到的话），就必须杜绝其通过糊弄的方式来蒙混过关的行为。因此，强制其通过 Lean 进行运作，无疑是实现这一目标的一个好方法。

毫无疑问，要想做到这一点，它们首先需要接受大量 Lean 代码的训练。幸运的是，像费马大定理和多项式 Freiman-Ruzsa 猜想这样的大型项目，恰好能生成大量这样的代码。

艾萨克·牛顿研究所的“大证明”项目

证明形式化是数学中一个活跃的研究领域，吸引了数学领域最杰出的一些学者。为这一领域的奠基起到关键作用的是，剑桥大学艾萨克·牛顿数学科学研究所（Isaac Newton Institute，INI）于 2017 年开展的一项研究计划，名为“大证明”（Big Proof）。在 2017 年首次"大证明"会议上，大多数与会者并非数学家，而是计算机科学家。艾萨克·牛顿数学科学研究所率先意识到了证明助手对数学未来发展的重要性，在这方面走在了时代前列。

然而，尽管与会数学家人数或许较少，但是这次会议仍然产生了深远影响。凯文·巴扎德坦言，正是汤姆·哈尔斯（Tom Hales）在会议上的演讲激励他投身当前的研究：“我听了汤姆·哈尔斯的首场讲座，他使用的工具与我相同，但他谈论的想法是如何使用这些工具开展现代数学研究……当时我刚刚花了两周时间证明完根号 2 是无理数，我看着这些幻灯片，心想，‘如果能在这个系统中做高等代数几何，岂不是很棒吗？’”

时光流转来到 2025 年，最新一届“大证明”会议最近如期举行。这一次，许多数学家处于各自领域的最前沿（尽管只有三位菲尔兹奖得主）。形式化数学的梦想正焕发着蓬勃生机。根据巴扎德所说，其本科阶段的知识体系中，目前仅剩两个小部分尚未用 Lean 编码，而这一领域只会不断扩展！

展望未来

在展望证明助手将如何塑造数学的未来时，我们不宜一概而论。然而，如果允许我们持乐观态度的话……在未来大语言模型的辅助下，形式化证明助手或许真的有机会赶上现代数学。大卫·希尔伯特曾梦想将所有数学形式化，而借助证明助手，这一梦想很有可能真的会成为现实。此外，又有谁知道，我们的数学树上是否还有我们尚未发现的遗漏分支？而当人工智能完全掌握 Lean 的所有能力时，谁又能预料它可能会创造出怎样的奇迹呢？

本文转载自微信公众号“中科院物理所”，原题目为《数学界来了个“顶级杠精”，专治各种证明不服！》，https://plus.maths.org/content/proof-assistants-part-1 。

原创 Watkins  返朴  2025 年 11 月 5 日 07:59  北京