6. 四色猜想及其计算机证明
四色猜想、费马猜想和歌德巴赫猜想，通常被称为世界三大数学猜想，也是世界三大数学难题。
四色猜想于1976年由美国数学家阿佩尔(Kenneth Appel)与哈肯(Wolfgang Haken)借助计算机完成了证明，遂称四色定理；费马猜想于1994年由英国数学家安德鲁 怀尔斯（Andrew Wiles）完成了证明，遂称费马大定理；哥德巴赫猜想尚未解决，目前最好的成果是1966年由中国数学家陈景润给出的（称其为陈氏定理：任何一个大于6的偶数，都可以表示成一个素数及两个素数乘积之和，简记为1+2），故歌德巴赫猜想还不能称为哥德巴赫定理(1+1)。这三个问题的共同点就是说起来简单易懂，但内涵深邃无比，困扰了一代代全球的数学家。
1852年，英国青年古色里（Francis Guthrie）提出了四色问题猜想：对平面或球面上的任意一个地图着色，至多用四种颜色就可以使相邻（即有一段公共边界而不是一点或有限点）两个国家或地区（这里所谓的“国家”或地区是指连通的区域）的颜色不同。在这里，古色里提出的问题是“任意的地图”，它不仅是全世界所有的可能的地图，也包括可以想象的地图，因而四色猜想的证明，需要给出对所有情况都适用的证明。用数学语言表示这一问题，则是“将平面任意地细分为不相重叠的区域，每一个区域总可以用1、2、3、4这四个数字之一来标记，而不会使相邻的两个区域有相同的数字。”

四色定理示意图

1872年，英国当时最著名的数学家凯利正式向伦敦数学学会提出了这个问题，于是四色猜想成了世界数学界关注的问题，世界上许多一流的数学家都纷纷参加了四色猜想的大会战。1878～1880年两年间，著名的律师兼数学家肯普和泰勒两人分别提交了证明四色猜想的论文，宣布证明了四色定理，大家都认为四色猜想从此也就解决了，但被后人检查出漏洞。经过人们的补救，肯普的方法可以证明“五色定理”。在证明过程中，肯普引入了图形可约性的概念及其检验方法，经过后人的推广，成为最后解决四色猜想的有力武器。后来，越来越多的数学家虽然为此绞尽脑汁，但一无所获。于是，人们开始认识到，这个貌似容易的题目，其实是一个可与费马猜想相媲美的难题。

进入20世纪，科学家们对四色猜想的证明基本上是按照肯普的想法进行的。1913年，伯克霍夫在肯普的基础上引进了一些新技巧，美国数学家富兰克林于1939年证明了22国以下的地图都可以用四色着色。1950年，有人从22国推进到35国，德国数学家希尔创建了“放电法”，为四色猜想的计算机证明奠定了基础。1960年，有人又证明了39国以下的地图可以只用四种颜色着色；随后又推进到了50国。看来这种推进仍然十分缓慢。电子计算机问世以后，由于演算速度迅速提高，加之人机对话的出现，大大加快了对四色猜想证明的进程。1970年左右，问题归结为计算几千个不可约构形的问题，但其计算量之大是难以想像的，因此人们仍望而生畏。

1975年，美国伊利诺思大学数学教授阿佩尔（K.Appel）与哈肯（W.Haken）多次改进自己的实验设计，开始对四色猜想进行计算机证明。他们发展了一种放电过程，以便产生由可约构形组成不可避免集，还编写了证明可约性的程序。1976年，阿佩尔与哈肯在美国伊利诺斯大学的两台不同的电子计算机上，用了1200多个小时，作了100多亿次判断，分析了两千多个构形的可约性，并通过人工分析了约一万个带正电顶点的邻近区域，终于用不可避免组的方法证明了四色问题，完成了四色定理的证明。四色猜想的计算机证明，轰动了世界，它不仅解决了一个历时一百多年的难题，而且有可能成为数学史上一系列新思维的起点。当两位数学家将他们的研究成果发表时，当地的信封上盖“Four colors suffice”（四色足够）的邮戳，以庆祝这一难题获得解决。
阿佩尔与哈肯的证明方法是将地图上的无限种可能情况减少为1936种状态（稍后减少为1476种），这些状态由计算机一个挨一个的进行检查。这一工作又由不同的程序和计算机独立的进行了复检。1996年，Neil Robertson、Daniel Sanders、Paul Seymour和Robin Thomas使用了一种类似的证明方法，检查了633种特殊的情况。这一新证明也使用了计算机，如果由人工来检查的话是不切实际的。
“四色问题”的证明不仅解决了一个历时一百多年的难题，而且成为数学史上一系列新思维的起点。它表明，靠人与机器合作，有可能完成连最著名的数学家至今也束手无策的工作，标志着人类认识能力的一个飞跃，极大地推动了以计算机为基础的人工智能的发展。在“四色问题”的研究过程中，不少新的数学理论随之产生，也发展了很多数学计算技巧。如将地图的着色问题化为图论问题，丰富了图论的内容。不仅如此，“四色问题”在有效地设计航空班机日程表，设计计算机的编码程序上都起到了推动作用。不过不少数学家并不满足于计算机取得的成就，他们认为应该有一种简捷明快的书面证明方法。直到现在，仍有不少数学家和数学爱好者在寻找更简洁的证明方法。
四色定理是第一个主要由计算机证明的定理，这一证明并不被所有的数学家接受，因为它不能由人工直接验证。最终，人们必须对计算机程序的正确性以及运行这一程序的硬件设备充分信任。首先，他们的“证明”，计算机程序就达400多页，要用人工去检验其程序有无问题是十分吃力的。因此，似乎无人愿意再去重复阿－哈的“证明”。其次，能否保证计算机在计算过程中绝对不出错误？第三，人们无法确定计算出现错误是计算机本身的机械或电子方面的毛病，还是“证明”过程本身逻辑有问题。缺乏数学应有的规范成了另一个方面；以至于有人这样评论“一个好的数学证明应当像一首诗——而这纯粹是一本电话簿！”于是就引起了什么是“数学证明”的争论。
有些数学家认为数学证明只能是以人工可重复检验的逻辑演绎(计算也是一种演绎)过程，否则只能称为计算机证明，二者不能混为一谈。因此，按这种观点，“四色问题”只能称已得到了计算机证明，而不能称已得到了数学证明。但是，另一些数学家反驳说，用人工来检验也可能产生错误。例如，数学史上曾有不少数学家(如意大利的Saccheri，法国的Legendre)声称他们已“证明”了欧几里得第五公设(即欧氏平行公理)。但后来发现他们的“证明”均有问题，其主要错误在于他们利用了与第五公设等价的命题，因此从逻辑上说他们都犯了循环论证的错误。
另外人工逻辑演绎证明可以重复吗？众所周知，群论中有一个著名的所谓有限单群的分类定理，单群的概念是由伽罗华 (Galois)在1830年最初给出的。一百多年来数学家企图对单群进行分类，直至20世纪80年代，由100多位数学家组成的非正规“队伍”，他们共同努力列出所有的单群并证明这样的列举是完全的。在花费了成千上万个小时以及发表了几百篇论文之后，这项工作才得以完成，证明长达15000多页!试问谁还愿意(或说可能)去重复他们长达15000多页的证明?
2005 年，Gonthier 建立了四色定理的全部计算机化证明。这一证明和阿佩尔的证明虽然都用到了计算机，但是其意义则根本不同。阿佩尔的证明本质上仍然是传统证明，计算机只是起到了辅助计算的作用，而 Gonthier 的证明则是纯粹的计算机证明，其每一步逻辑推导都是由计算机完成的。
虽然四色定理证明了任何地图可以只用四个颜色着色，但是这个结论对于现实上的应用却相当有限。现实中的地图常会出现飞地，即两个不连通的区域属于同一个国家的情况（如美国的阿拉斯加州），而制作地图时我们仍会要求这两个区域被涂上同样的颜色，在这种情况下，四个颜色将会是不够用的。

四种颜色染色的中国大陆分省地图