Euler's Eyes
2026-10-26
写给机器的记号：由计算机核验的证明
两千年来，数学证明一直是写给人读的文本。它可以跳过“显然”的步骤，可以借助图形，可以使用群体内部的约定。其余的由读者补全。近五十年来，出现了一位什么都不补全的读者：计算机。
四种颜色
给任意一张地图着色，使相邻的国家颜色不同，需要几种颜色就够了？答案是四种，这一猜想于 1852 年提出，抵抗了一个多世纪。1976 年，伊利诺伊大学的肯尼斯·阿佩尔和沃尔夫冈·哈肯证明了它：他们把问题化为将近两千种情形，由计算机逐一检验，用了一千多个小时的机时。
学界产生了分歧。一个没有人能够完整读完的证明，还算是证明吗？支持者提醒说，许多很长的证明也没有人完整读过；批评者说，程序可能有错误。2005 年，法国人乔治·贡蒂耶把整个证明，包括计算机的部分，写进了一个名为 Coq 的证明助手，它从公理出发检验每一个逻辑步骤。疑问换了地方：不再是“程序对吗？”，而是“检验器对吗？”——那是一个小得多、也容易审查得多的程序。
开普勒猜想
1611 年，开普勒断言，堆放橙子最密的方式就是水果摊上的金字塔。1998 年，美国人托马斯·黑尔斯宣布了一个证明，它把几百页的论证与大量计算机计算结合在一起。一组审稿人工作了四年，宣布他们对其正确性有“99% 的把握”。黑尔斯不满足于那 1%，启动了 Flyspeck 项目，用形式语言写出整个证明。2014 年，在几十位合作者的参与下，项目完成：机器检验了每一步。
Lean
如今数学家用得最多的证明助手是 Lean，由巴西人莱昂纳多·德·莫拉于 2013 年在微软研究院创造。围绕它形成了 mathlib，一个集体编写的库，收录了数十万条形式化的定理，作者有数百人。2020 年，德国菲尔兹奖得主彼得·舒尔茨向学界发起挑战，请大家把他的一个结果形式化，因为他自己也不确定是否核对过所有细节。“液态张量实验”（Liquid Tensor Experiment）于 2022 年完成：结果是对的，而且形式化过程还发现了证明中可以简化的地方。
Lean 的一行代码是这样的：
theorem soma_comuta (a b : ℕ) : a + b = b + a := Nat.add_comm a b
“对任意自然数 $a$ 和 $b$，$a + b = b + a$，证明就是库中的交换律定理。”什么都不省略：每个字母的类型，每一步的出处。这是把第7章的线性书写推向了极端，是把第4章中用文字写的证明译成了一种机器能够检验的语法。
练习：三种颜色不够的时候
一个中央国家被三个国家包围，而这三个国家中每一个都与另外两个接壤。证明这张地图需要四种颜色。
这四个国家两两接壤：中央的国家与三个都相邻，三个之间也彼此相邻。所以每个国家都需要一种与其他所有国家不同的颜色，必须用四种。定理保证的是，无论地图多复杂，都永远不需要五种。
练习：读懂那行 Lean
在 theorem soma_comuta (a b : ℕ) : a + b = b + a := Nat.add_comm a b 这一行中，指出假设、命题和证明。
(a b : ℕ) 声明字母：$a$ 和 $b$ 是自然数，就像文本中的“设 $a$、$b$ 为自然数”。冒号之后是命题 $a + b = b + a$。:= 之后是证明，这里只是引用库中一个已经证明的定理。我们在第 5 篇中见过的 Algol 的 :=，在这里带着新的意思再次出现：“定义为”，或“由……证明”。