无法被人类验证的证明，可以算是证明吗？
图片来源：《火影忍者》
撰文 | Jack Murtagh
翻译 | 岳楠楠
审校 | 栗子
在1852年，一个南非的数学家提出了一个看似简单实则引起无尽争议的问题。针对这个问题，有不少证明在发表后被推翻了，最终一个挑战数学基本原则的方案却解决了它。
这个引起诸多麻烦的颜色难题就是：如何用最少的颜色给地图着色，使相区域没有相同的颜色？以下是解决方法。请看下面的美国本土地图。
图片来源：June Kim
这个地图看上去有些简陋。为了让地图更生动，清晰地标示各地区的边界，制图师更愿意给它们着色，如下所示：
图片来源：June Kim
当然，我们不希望相邻的州使用同样的颜色，因为这会使边界更加模糊。在这种限制下，我们用了四种颜色来填充上面的地图。只用三种颜色可以吗？也许其他的地图需要五六种？
所谓地图，不一定都是体现真实区划的那种，只要是将一个平面分成多个区域的都可以算地图。问题是，对于任意一个给定的地图，填充它并使相邻区域拥有不同颜色，最少需要多少种颜色？有一些基本的规则：比如每个区域必须是连续的。所以从技术上讲，密歇根州是不符合的，因为密歇根湖将该州分成了两个不连通的部分。又比如被视为相邻的两个区域需要有共同的连续边界；仅在一个点（或多个离散的点）上相连则不被视为相邻。就像犹他州和新墨西哥州，他们只有一个点相接，因而不被视为相邻的区域。
基于以上规则，有一些问题的答案令人惊讶。假如打印一张包含几千个区域的复杂地图，需要多长时间来确定该地图是否可以用两种颜色上色？三种颜色呢？四种呢？不需要确定具体的着色方案，只需要确定是否存在一种方案满足要求。有趣的是，尽管这三个任务看上去几乎相似，但完成它们所需的时长完全不同。使用目前已知的最好方法：
· 想确定两种颜色是否足够满足上色要求，大约需要一个小时。首先，选择任一区域并为其选择一种颜色，比如红色。这将使所有跟他相邻的区域只能涂另一种颜色，比如蓝色。然后，这些区域的邻居涂红色，以此类推到整个地图。最终，要么有两个相邻区域涂了同一种颜色，则二色着色方案不存在；要么涂满了整片地图，都没有出现相邻区域同色的冲突，则二色着色方案存在。按照一秒涂1个区域的速度粗略计算，完成它需要50分钟。
· 假如地图不能只用两种颜色填充，判断是否需要三种颜色会花费更长的时间。一个下午会悄然流失。接着，当一周一周的时间从日历本上被撕下，你还在疯狂地画着无尽的组合，寻找一个可行的方案。再后来，为了继续未完成的任务，你不得不将它传给你的孩子，他们再传给他们的孩子。几代人全部奉献于寻找这张地图的三色着色方式，但毫无进展。直到数十亿年后，太阳不可避免地吞噬地球，结束这场愚蠢的努力，而我们与答案之间的距离几乎没有更近一步。判断任意地图能否以三色着色是困难的。这里的“困难”是指，它在技术上变成了一类以耗时闻名的计算问题，即NP完全问题 (NP-complete, Non-deterministic Polynomial-time complete)。对于这类问题，我们除了暴力搜索每个可能的着色方案外，没有更快的方法。随着地图中的区域个数增加，搜索空间呈指数增长。对于只有几个区域的小地图，我们还可以遍历每个可能的三色着色方式，直到找到一个可行的方案（或者得出不存在可行方案的结论）。但对于包含几千个区域的地图，三色着色的方案数量巨大，遍历是没有希望的。
图片来源：《炉石传说》
· 那么判断四种颜色是否可以填充地图需要多少时间呢？答案是，大约一秒钟，也就是你说一个“是”字所需的时间，因为每张地图都可以用四种颜色着色。这就是臭名昭著且备受争论的四色定理。
法兰西斯·古德里（Francis Guthrie）于1852年首次提出了四色问题的猜想。当时他注意到，以郡为着色单位的英格兰地图，只需要四种颜色就可以填充。他怀疑，这个规则可能适用于任何地图，但他和同事们都无法证明。显然，三种颜色并不是一直都够用。正如下图所示的情况，每个区域都与另外三个区域相邻，这种就不能只用三种颜色。
图片来源：June Kim
但是没有人能找到需要至少五种颜色的地图。著名数学家奥古斯塔斯·德摩根（Augustus De Morgan）痴迷于证明古德里的四色猜想，并陷入无法解决的困境。他甚至得出一个结论：为了解决这个问题，必须在数学基础当中增加一条新的公理才行。在数学上，公理是一个被假定为真而不需要证明的陈述，可以从中推导出更复杂的陈述。
表面上，这种狂热的挫败感在1879年结束了，当时出现了一个证明，表示四种颜色总是足够。一年后，另一个独立的证明又强化了这一点。论功行赏后，大多数数学家们重新被吸引回他们正常的研究中。但也有例外。在第一个证明发表11年后，两个证明都被推翻了，四色定理重新变回四色猜想。珀西·希伍德（Percy Heawood）指出了原始证明中的一个漏洞，但他也取得了一些进展，证明了五种颜色总是足够填充任何地图。这使数学界进入到了一个相当尴尬的境地。一个看似十分简单的问题，要在两个答案——4或5——之间二选一，但没人知道到底哪个是正确的。这种状态持续了将近一个世纪。
没有人能找到需要五种颜色的地图，但完全排除这种可能性仍是困难的。因为有无穷无尽的地图，一个人不可能逐个去检查它们。最终解决这个问题的一个关键技巧，就是将问题简化到了可以遍历的有限集。从无限到有限的飞跃是巨大的，但需要检查的情况数量之多仍远远超过了人力的范围。因此，数学家凯尼斯·阿佩尔（Kenneth Appel）和沃夫冈·哈肯（Wolfgang Haken）提出了一个大胆的想法：编写一个计算机程序来处理这些情况。1976年，经过几年的调试和一千多个小时的计算机计算后，他们的算法最终遍历了所有的情况，四色定理被证明了。这是第一个在证明中借助计算机的重要定理。
数学界被点燃了，庆祝与失望并存。阿佩尔和哈肯的同事之一，比尔·图特（Bill Tutte）为他们“击败了海怪克拉肯（Kraken）”而欢呼，而其他人则憎恶计算机对人类独创性的侵犯。这件事也给数学界带来了一个哲学问题。一个无法由人类验证的证明算不算是证明？许多人预计这项工作最终会被撤回，就像之前那两个被推翻的证明一样。《纽约时报》起初甚至拒绝报道这一消息，因为四色定理的证明“无论如何都是错的”。
图片来源：Pixabay
在接下来的几十年里，多次反驳计算机辅助证明的尝试都失败了。数学家们后来极大地简化了证明并验证了计算机代码，但直到今天，不借助计算机的证明还没有出现。四色定理现如今被广泛接受，但人们对它仍留有一种渴望。一个计算机程序可以系统地分析大量的着色方式，但它并不能解释“为什么”每个地图都可以被四色填充。尽管现在数学家越来越愿意接受计算机的辅助，但他们仍在寻找一个对这个颜色谜题更有启发性的证明。
原文链接：
https://www.scientificamerican.com/article/how-a-doodlers-problem-sparked-a-controversy-in-math/
《环球科学》9月新刊正在热卖
各电商平台均有销售
微信扫码关注该文公众号作者