如果我们移除这个顶点以及与之相连的所有边,我们就得到了一个有n个顶点的图,我们已经知道可以用四种颜色来着色。现在看一下与移除的顶点相邻的顶点。如果它们中的三个或更少是不同的颜色,我们可以把移除的顶点涂上剩下的一种颜色,这样就完成了:我们刚刚证明了具有n+1个顶点的图可以用四种颜色着色。如果相邻的顶点包含了所有四种颜色,肯普设计了“一种聪明的方法”来重新涂色特定的顶点,以释放一种颜色给移除的顶点,从而再次证明具有n+1个顶点的图只需要用四种颜色。1890年,数学家希伍德(Percy Heawood)发现了肯普的错误。在一种特殊情况下,肯普的聪明方法会失败。希伍德指出,肯普的技巧可以证明每个地图都可以用五种或更少的颜色来着色。希伍德还研究了在更复杂表面上绘制的图(刚刚我们讨论的都是平面图)。他证明了一个带有 g 个孔的甜甜圈图可能需这么多种颜色:因此,着色一个普通甜甜圈可能需要多达七种颜色的涂料。然而,他对一般曲面的证明是不完整的,直到1968年才有了一个完整的证明。1976年,在一次会议上,福尔克·哈肯(Wolfgang Haken)与肯尼斯·阿普尔(Kenneth Appel)合作,宣布解决了四色定理。然而,人们对此反应褒贬不一。因为他们的证明依赖于计算机,而不是一个书面证明。由于平面图的数量是无限的,因此他们没有让机器直接回答这个问题,因为计算机无法检查所有可能性。不过,肯普曾经证明每个图形都包含六个特殊的顶点配置,而阿普尔和哈肯则证明每个图形必须具有1936个特殊的配置。证明这个定理的过程就是要表明我们只需要四种颜色就可以给包含这些子图的任何图形着色。为了更细致地控制每种情况并使每种情况更容易检查,他们将肯普的六种特殊情况分解成了1936个子情况,尽管现在总数已经远远超出了人类在没有辅助工具的情况下验证的范围。事实上,完成这些计算需要超过1000小时的计算机时间。数学界对这些结果只是勉强接受,他们认为证明应该是可以被人类完全理解和验证的。尽管让计算机执行日常算术是可以接受的,但数学家并不准备将逻辑推理让给计算机。这种保守和不愿意接受新事物的现象并不是首次,类似的情况在17世纪也曾发生,当时一些数学家使用新颖的代数技巧来解决几何问题,引起了类似的争议。随着机器学习的兴起,同样的戏剧性场景可能会再次出现:数学家是否会接受由不透明算法发现和证明的定理?四色问题的证明只是计算机革命在数学中的开始。1998年,黑尔斯(Thomas Hales)通过使用计算机生成和验证大量的数学公式,最终证明了开普勒猜想(conjecture of Johannes Kepler’s)。他使用了复杂的计算机程序和算法,包括离散傅里叶变换、线性规划和自动定理证明。这项工作产生了几千页的证明文件,历时近10年才完成。