从四色定理到 OpenAI：计算机证明为何总被质疑

在OpenAI发布370多个“结果族”之后，知名数学家们提出了意义之问：AI辅助的数学在多大程度上还算是数学？一个由LLM主导、难以理解的证明该如何看待？

广告之后继续阅读

在本栏目中，我们每周二都会介绍来自IT、科学、艺术、经济、政治领域以及当然还有数学领域的令人惊讶、印象深刻、富有启发性和趣味性的数字。

所有“数字，请讲！”栏目文章

这些问题并不新鲜。50年前，Wolfgang Haken和Kenneth Appel发表了他们对四色定理的证明。该定理指出，四种颜色足以给任意地图着色，使得没有共同边界的国家使用相同的颜色。该证明由IBM 360-75、370-158和370-168型大型计算机在1200小时的运算时间内完成。证明的检验同样使用了一个独立的计算机程序。

世界上的国家被划分为四种颜色：按照四色定理着色。

（图片：Fibonacci，CC BY-SA 3.0，编辑：heise medien）

定理研究历时四年

这两位来自厄巴纳-香槟伊利诺伊大学的数学家为他们的四色定理证明工作了四年。他们延续了一个有着悠久传统的证明思路。因为四色定理源于数学家Francis Guthrie于1852年提出的一个猜想，当时他想给英格兰各郡的地图着色。1878年，数学家Arthur Cayley在伦敦数学学会的一次会议上提出了这一猜想。

律师Alfred Kempe参加了那次会议，并在一年后提交了一个证明。正如Haken和Appel在他们关于四色定理的论文中所阐述的那样，Kempe从猜想的反面出发，证明了它会导致矛盾。直到十一年后，这个证明才被推翻，但Kempe的方法，即所谓的Kempe链理论，为后来的数学家指明了方向。

南非数学家和植物学家Francis Guthrie（* 1831年1月22日生于伦敦；† 1899年10月19日卒于开普敦Claremont）于1852年在制图工作中得出了四色定理的猜想。

1922年，数学家们证明了每张拥有25个或更少国家的地图都可以用四种颜色着色。十年后，证明推进到了96个国家——随后，当Kurt Gödel的不完备性定理震撼数学界时，这一猜想被搁置一旁。究竟需要四种、六种还是两种颜色，Wayne其实并不关心？

广告之后继续阅读

1936年，数学家Heinrich Heesch开始研究四色定理。他拒绝加入纳粹德国讲师联盟，这终结了他的大学学术生涯，于是他以私人身份研究需要考察的可能地图和节点的数量。他估计大约有10,000种构型。战后，他就这一主题发表演讲，并作为汉诺威技术大学的教授与数学家Karl Dürre共同提出了一个检验可能组合的计算机程序的想法。

Heesch多次前往美国，因为当时在德国可用的计算机对于他的计划来说性能不够强大，他在那里与数学家Wolfgang Haken和Yoshio Shimamoto合作。后者于1971年发表了一个带有计算机程序的思路，但该程序存在错误。

Haken和Appel于1976年最终提出的证明十分复杂。1482种构型必须由计算机逐一计算，平均每种构型需要不到一小时的运算时间。在发表前负责审查该证明的评审专家们自己也动用了计算机。“当我们将关于该证明的论文提交给《伊利诺伊数学杂志》时，评审专家根据我们的完整材料检验了放电方法，同时他们通过使用一个独立的计算机程序验证了[所考察的1482种构型]的可约性计算”，Haken和Appel在他们的回顾中这样写道。

对计算机辅助证明的大量批评

证明首次发表后，引发了一片愤怒的声浪。纽约亨特学院的丹尼尔·科恩说：“把阿佩尔和哈肯的计算机辅助把戏纳入数学领域，只会让我们在智识上感到不满足。”剑桥大学的乔治·斯宾塞-布朗则猛烈抨击道：“这不是证明，这甚至算不上证明的开端。这是数学史上出现过的最可笑的‘皇帝的新衣’案例，让数学蒙羞。”宾夕法尼亚大学的组合数学家赫伯特·威尔夫说：“上帝不会允许这一定理通过如此可怕的方法得到证明！”

其他批评则属于当时所谓的“计算机技术”性质：如果计算机的编译器或操作系统在运行证明时存在错误，那该怎么办？数学界之外也出现了激烈的反应。《纽约时报》的科学编辑部拒绝发表一篇关于该证明的文章。哲学家托马斯·蒂莫奇科在《哲学杂志》上写道：“没有一位数学家见过四色问题的证明，同样也没有人见过证明该问题存在证明的证明。

此外，数学家亲眼看到四色问题证明的可能性极低。”蒂莫奇科以他自己的方式点明了这个难题：一个形式上严密、但人类无法纵览的证明，无法逐步检验其逻辑上的连贯性。

强烈的抵制促使哈肯和阿佩尔于1989年出版了一本书，其中包含更详细的论证，也收录了此前仅以缩微胶片形式发表的补充材料。数学史学家罗宾·威尔逊在其著作《四色足矣》中写道，对这一证明的拒绝或接受，几乎完全是一个年龄问题。40岁以下的数学家接受四色定理的计算机化解决方案，40岁以上的人则拒绝接受。这一规律的一大例外是生于1917年的英国密码学家和数学家比尔·塔特，他本人也曾提出过一种解决四色定理的思路。

1976年，他为庆祝这一证明而作诗道：“沃尔夫冈·哈肯击杀了海怪，一！二！三！四！他说道：怪物已不复存在。”

计算机技术作为证明助手

塔特富有远见地补充说，其他曾研究这一问题的数学家们想必会绝望地抓头发，并问自己：“我们现在到底该怎么办？”他的回答是：“保持勇气！你可以继续研究。你可以去研究哈约什和哈德维格的猜想。”还可以补充一点：这头怪物后来也被其他方法驯服了。1996年，尼尔·罗伯逊、丹尼尔·桑德斯、保罗·西摩和罗宾·托马斯将证明简化为633种构型。2005年，乔治·贡蒂埃在证明助手Coq中完成了该证明的完整形式化。他写道：“证明中其余约6万行内容虽然可以为了获取洞见甚至为了消遣而阅读，但不必再检验其正确性。这是证明助手Coq的任务——一项交给计算机的任务。”

随着OpenAI发布数百个AI生成的解决方案，这个问题被提升到了一个新的层面。《纽约时报》在一篇长文中描述了2006年菲尔兹奖得主陶哲轩如何从AI的热情使用者转变为对OpenAI做法的尖锐批评者，如今他在会议上指导自己的博士生，而据陶哲轩说，这些会议越来越像心理治疗。哈佛数学家的一份报告建议，未来授予博士学位时应减少对论文文本的看重，而更重视严格的 oral defense。

与近50年前的比尔·塔特相似，陶哲轩依然勇敢乐观、保持勇气，因为在数学的边界上还有许多未解决的问题。“这是一个属于创造力的时代，我非常希望学生们能迎接这一挑战。他们并没有主动要求这一切。但我相信，他们中的许多人会让我们惊讶。”最后，让我们以塔特的另一首诗作结：

“四色定理是冰山的一角，是楔子的薄端，是春天的第一只布谷鸟。”

（mawi）