定理证明有用吗（海韵教育四色定理的证明是真的）

四色定理指的是“在地图上分块涂色以区分相邻地区的话，只用4种颜色就足够”的定理。看起来似乎不难理解，但人们历经了124年的时间才证明了它。然而，其证明方法却引起了广泛的争论，甚至波及到哲学领域，并且给大众留下了“证明到底是什么？”这样的问题……

定理、公理和公式的区别是什么?

在解说四色定理之前，我们先来谈谈“定理”的意思。和定理相似的词还有“公理”和“公式”。

公理指的是作为数学基础的假设。例如，“由任意一点到另外任意一点可以画直线”就是一个公理的例子（欧几里得《几何原本》中的第1公设）。在公理的前提下推导出的事实被称为定理，而对于用数学式来表示的定理又被称为公式。

在数学里，经常会听到“○○问题”“△△猜想”这样的说法，它们指的是尚未被证明的定理或者公式。美国的克雷数学研究所（Clay Mathematics Institute）宣布的“千禧年大奖问题”就非常有名。发布时总共有7个未解决的问题，每个问题都悬赏100万美元。截至目前，其中只有庞加莱猜想得到了证明。

四色定理在被证明之前，被称为“四色问题”。那我们从这里，也先把它称为四色问题吧。对于定理和问题，如果能够给出它是“正确的还是错误的”(真伪）之一的答案的话，又能被称为“命题”。具体到四色问题，因为需要证明它的真伪，所以它也是一个命题。

四色问题是针对平面上绘制的地图分块涂色区分加以考虑的。使用现实中的地图也可以，自己想象的地图也可以。让我们准备好纸和彩色铅笔，按照自己的想法先画地图，再用彩色铅笔试试进行分块涂色区分吧。要注意，这时候相邻的区域一定需要用不同的颜色填涂。但是，如果两个区域只有一个点相接的话，不被认为是相邻区域。比如下图所示的美国地图里，当州界呈十字交错时，对角的两个州用同一种颜色填涂是可以的。

那么，你成功地用4种颜色分块涂色区分了你所画的地图了么？如果用了5种或者更多种颜色，那不是因为四色定理是错误的，而肯定是填涂方法出了问题。

另外，如果不是在平面上，而是对在像甜甜圈一样的立体表面上绘制的地图进行分块涂色区分的话，最多需要7种颜色（下图）。也就是说，对于在有空洞的立体表面上绘制的地图分块涂色区分，可能要用到超过4种颜色。不过，对于像地球这种没有空洞的立体，其表面上的地图分块涂色，同样只需要4种颜色就足够区分。

当考虑在像甜甜圈这样有一个空洞的立体表面（环面）上绘制地图时，对相邻区域涂色区分最多需要7种颜色。此定理在1890年由英国数学家希伍德证明。

四色问题很快就被解决了？

四色问题是在距今大约170年前的1852年，由当时还是学生、后来成为数学家的弗朗西斯·格思里（Francis Guthrie，1831～1899）提出的。他的弟弟、之后成为物理学家的弗雷德里克·格思里（Frederick Guthrie，1833～1886）知道了这个问题后，向他的老师、当时的英国数学家奥古斯塔斯·德·摩尔根（Augustus De Morgan，1806～1871）询问了四色问题是否正确。

收到这个问题的德·摩尔根写信向爱尔兰的数学家、物理学家威廉·哈密顿（William Hamilton，1805～1865）询问。但是，哈密顿的反应却不冷不热。四色问题在当时只受到了包括德·摩尔根在内的数名数学家的关心。之后，德·摩尔根在问题得到证明之前就于1871年去世，四色问题也随之被世间暂时遗忘。

到了1878年，英国既是数学家又是律师的阿瑟·凯利（Arthur Cayley，1821～1895）在伦敦数学学会再次提出了这个问题，让四色问题重见天日。此时，英国的业余数学家艾尔弗雷德·肯普（Alfred Kempe，1849～1922）得知了这个问题，并很快就宣布解决了四色问题。

肯普独创了被称作“肯普链”的方法，并认为用这种方法能够成功证明四色问题。相关论文在次年的1879年刊载于《美国数学期刊》。不过，虽然当时大家都相信他的证明正确无疑，但其实他的证明里有一个重大的错误。在没有人注意到这个错误的情况下，在十多年间大家都相信肯普的证明是正确的。

1890年，英国数学家珀西·希伍德（Percy Heawood，1861～1955）指出了肯普证明里的错误。他也是证明了环面上的地图最多只需要7种颜色来填涂区分的人。希伍德虽然指出了肯普证明里的错误，但是他也并没能证明四色问题本身。取而代之的是，他利用肯普的思路，证明了在平面或球面上绘制的地图，最多只要有5种颜色就能填涂区分（五色定理）。

希伍德的指摘引起了大家的注意，就算正确性被深信不疑的证明也会出现错误。这之后，大家认识到四色问题是一个非常困难的问题，以至于在此后近百年间，四色问题一直让数学家为之烦恼。

用“点”和“线”抽象思考地图?

对于四色问题，实际上可以用一个很有效的方法来思考。首先，在由边界线包围的各个区域里放置一个“点”，再把相邻区域里的点用线连接起来（下图）。比起原本纷繁复杂的地图，这样抽象化后，理解起来能更加简洁吧。像这样只利用点和线来表示各种“连接关系”的理论被称为“图论”，是一种对组合问题进行简洁记述的有效手段。

在地图的各个区域里放置一个点，再把相邻区域里的点用线连接起来。像这样，把物体的相邻关系用点和线来表示的数学理论称作“图论”。

这样的点线图不太好直接涂色，取而代之的是对点赋予数字（0，1，2，3……）来标记。由于通过线相连的2个点表示相邻的意思，所以不能赋予相同的数字。通过以上这般思考的话，四色问题就可以转变成“对于在平面上绘制的点线图，如果要给通过线相连的2个点赋予不同数字的话，4个数字（0，1，2，3）是否足够”这样的命题。

另外还有一点需要说明，在思考四色问题时，必须用到一个定理。这就是由瑞士数学家莱昂哈德·欧拉（Leonhard Euler，1707～1783）提出的“多面体欧拉定理”。这个定理说的是，对于没有空洞的多面体而言，顶点的数目和平面的数目相加，再减去边的数目，一定等于2。例如，对于骰子这样的立方体，顶点的数目是8，平面的数目是6，边的数目是12，所以有8＋6－12＝2，也即符合多面体欧拉定理。

不仅如此，多面体欧拉定理对于平面地图同样适用。也就是说，对于平面地图抽象而成的点线图也能成立。在这种情况下，点的数目和由连线围起来的区域的数目相加之后，减去连线的数目，结果即为2。如上图中，点的数目是11，由连线围起来的区域数目是7（所有连线之外的区域也算1个区域），连线的数目是16，所以11＋7－16＝2, 也验证了多面体欧拉定理。

到1940年，通过基于多面体欧拉定理的方法，大家知道了对于由少于等于35个国家组成的地图来说，只用4种颜色就可以填涂区分了。

解决四色问题的手段

不过，四色问题需要证明的是，无论什么样的世界地图都可以用4种颜色填涂区分。如果一个一个地去确认36个国家、37个国家、38个国家……的地图，证明永远不能确立。因为国家的数目可以无限增大。

因此，数学家开始尝试假设“四色问题不成立”。如果四色问题不成立的话，那就一定存在用4种颜色不能填涂区分的地图。基于这样的假设来思考四色问题的话，如果找不到用4种颜色无法填涂区分的地图，就能导出结果与假设相矛盾。如果确认矛盾的话，那就说明最开始的假设（四色问题不成立）是错误的。换句话说，四色问题就被证明是成立的。像这样，为了证明某个命题而先假定这个命题不成立，并在此基础上导出矛盾从而证明这个命题的方法，叫做“反证法”。

美国数学家肯尼思·阿佩尔（Kenneth Appel，1932～2013）与德国数学家沃尔夫冈·哈肯（Wolfgang Haken，1928～）基于反证法考查了各种各样的图。可是，他们发现了这样做的工作量非常庞大，需要花费很多时间。于是，他们决定使用电子计算机来进行验证。

四色问题的证明是真的“证明”吗?

这两位数学家对大约2000种的点线图模式（下图），先是人工运算，然后使用了3台电脑（包含当时最先进的电脑），进行了验证。计算时间总计约花费1200小时，打印了计算结果的纸张垒起来高达1.2米。

证明四色定理时需要考察的点线图的部分例子。这里绘出的点线图，就像拼图游戏的小块一样，只是某些点线图里的一部分。红色的点表示有5条连线（有 5个邻国）。虽然图中大部分点的连线没有画完全，但如果恢复成原本的点线图，每个点所含的连线数目都会补足。阿佩尔和哈肯使用计算机对大约2000种这样的点线图进行了考察。

如果这些计算结果是正确的话，就会和最初的“四色问题不成立”的假设相矛盾，从而达到证明四色问题的目的。之后，由其他数学家对这些计算结果的正确性进行了验证后，四色问题终于得到了证明。这时，已经是离弗朗西斯·格思里提出问题124年之后的1976年了。

但是同时，对于这样使用了计算机进行了大量计算并以计算结果作为证明的方法，出现了很多批判的声音。这是因为，当时大家认为对于数学而言，证明应该是能用人的手和脑来“简洁优美”地完成的事情。关于这一证明方法的争论，一直波及到哲学领域，并且给大众留下了“证明到底是什么？”这样的问题。

四色问题被证明后，终于得以被正式地称为“四色定理”。但是，不用计算机，而只用纸和笔的简洁优美的证明目前还尚未成功。从这个角度来说，或许也可以把它称为某种程度上尚未解决的问题。

现在，四色定理还被应用于配置移动电话基站位置这一领域。为了不让频率完全相同的基站相邻，需要对基站的频率配置加以“填涂区分”。看着好像和我们的生活没太大关系的数学定理，其实一直活跃在日常生活中。