1976年7月，一个让数学家困惑了一个多世纪的数学谜团终于被解决了：四色定理。四色定理声明：给任何地图上区域着色至多需要四种颜色，以确保没有两个相邻的区域具有相同的颜色。它的作者肯尼斯·阿佩尔和沃尔夫冈·哈肯将一位非传统的合作者归功于计算机，实际上是计算机完成了大量的数学工作，确切来说是1200小时的计算和100亿次的决策。计算机程序员约翰·科赫帮助阿佩尔和哈肯进行算法工作。阿佩尔和哈肯后来描述了系统如何“开始教会我们一些我们从未预料到的前进方式”，承认在某些智力任务上该系统“超过了其创造者”。一个人与机器数学的勇敢新世界开始了，这引发了一个问题：我们是否能够相信一个数学证明，其规模太大而任何人都无法验证？数学家的反应从接受到拒绝，甚至否认——而不是普遍的崇拜。自视理性的数学家们，突然面临一个数学的巨兽，这感觉就像异教徒的亵渎。 “上帝不会让这个定理以如此糟糕的方式被证明！”——赫伯特·威尔夫，宾夕法尼亚大学一些人抗议没有数学推理的数学证明，并对此发声：“目前的证明实际上依赖于一个神谕，而我说神谕应当被抛弃！它们不是数学”……——保罗·哈莫斯，加州大学圣巴巴拉分校“如果解决方案涉及计算机对特殊情况的验证……这样的解决方案根本不属于数学科学。”——弗兰克·邦索尔，爱丁堡大学“承认阿佩尔和哈肯的计算机戏法进入数学的行列，只会让我们在智力上感到不满足。”——丹尼尔·科恩，纽约亨特学院其他人拒绝相信根本找到了证明：“不仅在他们发布的东西中找不到任何证明，甚至没有任何东西开始看起来像证明……这是有史以来最可笑的‘国王的新衣’案例，让数学史上蒙羞”——乔治·斯宾塞-布朗，剑桥大学一位数学系主任拒绝让阿佩尔和哈肯见他的研究生，声称他们的方法消除了找到一个可验证且更加优雅的证明的动力：“既然问题是以完全不当的方式解决的，任何一流的数学家现在都不会再对此进行研究，因为他不会再是第一个做到这一点的人，因此一个体面的证明可能会无限期推迟。”（由罗宾·威尔逊在《四色足够》中叙述）有趣的是——也是意料之中——年龄似乎是对计算机辅助证明的接受度的决定性因素。在哈肯的儿子关于证明的演讲之后（他帮助父亲完成这项工作），观众据说分成了两组：“40岁以上的人无法相信计算机证明是正确的，而40岁以下的人无法相信包含700页手工计算的证明是正确的。”（来自罗宾·威尔逊的书《四色足够》）该证明赢得了一些高端的背书。传奇数学家比尔·图特——曾在一份期刊中公开质疑他们的计算机辅助方法——会承认其解决方案，并用一首诗来庆祝：沃尔夫冈·哈肯打击了克拉肯！一！二！三！四！他说：“怪物不再存在。”受人尊敬的德国数学家海因里希·海施勉强接受了这个证明——因为他花了四十年解决这个问题，甚至创造了阿佩尔和哈肯使用的关键算法方法。其他数学家也认真对待这个证明，比如特德·斯瓦特——他在同一时间内正在接近一个计算机辅助证明——却被抢先一步。高端的背书帮助该证明获得了可信度并成为头条新闻，除了《纽约时报》，其编辑因担心这是虚假警报而拒绝报道这一突破。一旦几个月后被认为是合法的，编辑们认为这已经不再具有新闻价值。它仅因美国数学学会会长利普曼·伯斯的一篇专栏文章而出现在公报中。关于“没有推理的证明”的争论在1979年加剧，哲学家托马斯·提莫兹科在《哲学杂志》中辩称，一个无法调查的证明不是传统的数学证明（尽管他并不怀疑该证明在技术上证明了它所声称的内容）“没有任何数学家见过四色定理的证明，也没有人见过证明其有证明的证明。而且极不可能有任何数学家能看到四色定理的证明。”——托马斯·提莫兹科特·斯瓦特将在《美国数学月刊》中回应提莫兹科，他后来总结自己的论点说：“我认为计算机辅助证明只是铅笔和纸的延伸。”