两千年来，数学证明一直是写给人读的文本。它可以跳过“显然”的步骤，可以借助图形，可以使用群体内部的约定。其余的由读者补全。近五十年来，出现了一位什么都不补全的读者：计算机。 四种颜色 给任意一张地图着色，使相邻的国家颜色不同，需要几种颜色就够了？答案是四种，这一猜想于 1852 年提出，抵抗了一个多世纪。1976 年，伊利诺伊大学的肯尼斯·阿佩尔和沃尔夫冈·哈肯证明了它：他们把问题化为将近两千种情形，由计算机逐一检验，用了一千多个小时的机时。 一张用四种颜色着色的地图，任何两个相邻的区域颜色都不相同。Inductiveload · 维基共享资源 · CC BY-SA 3.0 学界产生了分歧。一个没有人能够完整读完的证明，还算是证明吗？支持者提醒说，许多很长的证明也没有人完整读过；批评者说，程序可能有错误。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章中用文字写的证明译成了一种机器能够检验的语法。 改变群体的记号 形式化正在改变工作方式。像英国人凯文·巴扎德在 2024 年发起的费马大定理形式化这样的项目，聚集了几十位从未谋面的合作者，每人形式化一个引理，并确信各个部分能拼合在一起，因为接缝由机器来检验。记号再一次决定了谁能参与、怎样参与。