四色定理：机器首次困扰数学家

1976 年 7 月，一个困扰数学家一个多世纪的数学谜题终于得到了解答：四色定理 * *四色定理指出：为任何地图的区域着色不需要超过四种颜色，这样相邻的两个区域就不会具有相同的颜色。它的作者 - 肯尼斯·阿佩尔 (Kenneth Appel) 和沃尔夫冈·哈肯 (Wolfgang Haken) - 将归功于一位非传统的合作者：计算机完成了大部分数学繁重工作，进行了 1,200 小时的计算和 100 亿次计算准确的决定。计算机程序员约翰·科赫 (John Koch) 将帮助阿佩尔和哈肯进行算法工作。阿佩尔和哈肯后来描述了该系统如何“开始教我们如何进行我们从未预料到的事情”，并承认该系统在某些智力任务中“超越了其创造者”。一个勇敢的人机数学新世界已经开始，它引出了一个问题：我们是否应该相信一个数学证明对于任何人来说都无法验证？数学家的反应从接受到拒绝，甚至否认，而不是普遍崇拜。以理性为荣的数学家们突然遇到了一个数学莫洛赫，这一定让人感觉像是非宗教的异端邪说。 “上帝不会让这个定理用这样可怕的方法来证明的！” - Herbert Wilf，宾夕法尼亚大学 有些人抗议没有数学推理的数学证明，并大声疾呼：“目前的证明实际上依赖于神谕，我说打倒神谕！它们不是数学”…… - Paul Halmos，加州大学圣塔芭芭拉分校“如果解决方案涉及特殊情况的计算机验证……这样的解决方案根本不属于数学科学。” - Frank Bonsall，爱丁堡大学“将阿佩尔和哈肯的计算机恶作剧纳入数学行列只会让我们在智力上得不到满足。” - 丹尼尔·科恩，纽约市亨特学院 其他人根本不相信已经找到了证明：“他们发表的文章中不仅找不到任何证据，而且连任何看起来都不像证明的东西……这是‘国王的新衣’最荒谬的例子，它让数学史蒙羞。” - 乔治·斯宾塞-布朗，剑桥大学 一位数学系主任拒绝允许阿佩尔和哈肯与他的研究生见面，声称他们的方法已被删除寻找可验证且更优雅的证明的动机：“由于这个问题是通过完全不适当的方式解决的，所以现在没有一流的数学家会再研究它，因为他不会是第一个这样做的人，因此一个像样的证明可能会被无限期地推迟。” （罗宾·威尔逊在《四种颜色就足够了》中叙述）有趣的是——而且可以预见的是——年龄似乎是接受计算机辅助校样的决定性因素。据报道，在哈肯的儿子介绍了这个证明（他帮助他父亲完成）之后，观众分成了两组：“40 岁以上的人无法相信计算机证明是正确的，而 40 岁以下的人则无法相信包含 700 页手工计算的证明是正确的。” （来自罗宾·威尔逊（Robin Wilson）的书《四种颜色就足够了》）该证明将赢得一些高调的认可。传奇数学家比尔·塔特（Bill Tutte）曾在期刊上公开质疑他们选择的计算机辅助方法，他承认这个问题已得到解决，并用一首诗来庆祝：沃尔夫冈·哈肯（Wolfgang Haken）击杀海妖！二！三！四！他说：“怪物已经不复存在了。”受人尊敬的德国数学家海因里希·希施（Heinrich Heesch）不情愿地接受了这个证明——因为他花了四十年的时间研究这个问题，甚至创造了阿佩尔和哈肯应用的关键算法方法。其他数学家也认真对待这个证明，比如泰德·斯沃特（Ted Swart）——他大约在同一时间接近计算机辅助证明——却被打败了。高调的支持帮助这一证据获得了可信度并成为头条新闻，但《纽约时报》除外，该报的编辑拒绝报道这一突破，因为担心这是一场虚惊。几个月后，一旦它被认为是合法的，编辑们就认为它不再具有新闻价值。由于美国数学会主席利普曼·贝尔斯 (Lipman Bers) 的一篇专栏文章，它才出现在记录论文中。关于“无需推理的证明”的争论在 1979 年愈演愈烈，当时哲学家托马斯·蒂莫茨科 (Thomas Tymoczko) 在《哲学杂志》上指出，不可检验的证明不是传统的数学证明（尽管他并不怀疑该证明在技术上证明了它所声称的内容）“没有数学家见过 4CT 的证明，也没有见过它有证明的证明。此外，任何数学家都不太可能看到 4CT 的证明。” 4CT。” - 托马斯·蒂莫茨科（Thomas Tymoczko） 泰德·斯瓦特（Ted Swart）在《美国数学月刊》上发表的一篇回应中反驳了蒂莫茨科，他后来总结自己的论点说：“我认为计算机辅助证明只是铅笔和纸的延伸。”