四色定理迎来罕见新证明

引言

有些数学问题即使已经解决，仍会让研究者念念不忘。证明早已问世，甚至一度广受赞誉，但不满依然挥之不去——或许是论证太过繁复，让人仍在追寻那篇梦寐以求的一页纸证明；或许是它没能揭示更深层的理论缘由，说明结论为何成立。不管出于什么原因，数学家们总会一次次回到这个本已被认为盖棺定论的问题上。

其中最著名的例子之一就是四色定理，它彻底改变了数学家对本学科的思考方式。

这个问题表述起来很简单，甚至一眼就能看懂：给定一张连续的地图，能否只用四种颜色给每个区域上色，使得相邻区域颜色不同？19 世纪中叶，制图师们对这个问题毫无兴趣——他们手里的颜色远不止四种，也没觉得有什么必要限制自己的调色盘。但对业余爱好者和职业数学家来说，这道脑筋急转弯很快变成了一种执念。

1879 年公布的第一个所谓证明维持了 11 年，最终被证明是错误的。此后错误答案接踵而至，出自律师、医生，甚至著名图论学家之手。“这是一个连小孩子都能理解的问题，”丹麦技术大学的图论学家 Carsten Thomassen 说，“我想这正是它成为如此巨大挑战的原因。”

这个定理直到近一个世纪后才被证明——但当时所使用的计算机方法被视为不可接受的，令数学家们质疑什么才算作证明。直到1997年，随着计算机应用变得更为普遍，一个更简洁的计算机辅助证明被找到，该问题的地位不再引起争议。

然而，即使在今天，哥本哈根大学计算机科学家 Mikkel Thorup 所称的“四色病”仍在传播。他和 Thomassen 都认为自己是受害者。如此简单的陈述，其成立的理由理应更简单。或者至少存在一种更高效的方法来证明它。

经过近十年的工作，Thorup、Thomassen 以及丹麦、加拿大和日本的四名同事，为该定理提供了另一个计算机证明。

这项证明——于2026年3月在线发布，并将在十一月的计算机科学基础年会上展示——在某些方面比其前驱更为复杂。“他们似乎在证明过程中大量使用了电力，”巴黎 Inria 的计算机科学家 Georges Gonthier 说道。但在构建论证的过程中，研究人员提供了一种为地图着色的远更高效的方法。通过这样做，他们揭示了被称为平面图的重要数学对象的结构性新见解——为图论中许多其他顽固问题的进展打开了大门。

考虑到这一问题曾屡遭失败、屡屡令人失望，龚希尔（Gonthier）表示：“能终于见到一个真正的结果，实在令人振奋。”

计算机化的争议

1852 年，数学家弗朗西斯·古德里（Francis Guthrie）在给英格兰郡的地图着色时，发现只需四种颜色便足够。他不禁好奇，这是否永远如此？他向同为数学家的弟弟弗雷德里克（Frederick）请教，弗雷德里克的导师奥古斯都·德·摩根（Augustus De Morgan）对此问题产生了兴趣，并决定向更广泛的受众推广这一议题。到了 1879 年，当数学家阿尔弗雷德·布雷·肯普（Alfred Bray Kempe）声称找到了解法时，媒体通过 Nature 发布了这一成就的消息。

肯普首先假设结论的反面：存在一张地图无法仅用四种颜色着色。随后，他试图证明这一假设最终会导致矛盾——这意味着这样的地图根本不存在。倘若如此，所有地图就必然可以被四种颜色着色。

首先，他说，想象你假设的那张无法用四种颜色着色的地图尽可能“最小化”：如果从其中移除任何一国，剩下的地图就能用四种颜色着色。接着，通过将地图重绘为所谓的平面图，剔除地理等其他次要细节。将每个国家表示为一个点（或顶点），若两个国家接壤，则在两点间画一条线（或边）。你的地图着色问题如今变成了图着色问题，从而可以借用图论的工具来解决。

特别值得一提的是，早在 18 世纪，瑞士数学家莱昂哈德·欧拉（Leonhard Euler）就发现平面图拥有许多实用性质——其中包括一个保证：任何此类图都至少包含一个拥有五个或更少邻居的顶点。这意味着，你的图中必定包含以下六种构型中的一种，肯普将其称为“不可避免集合”（unavoidable set）：

由于你的图是极小图，从中删去任何一个构形，剩下的图都能用四种颜色重新着色。Kempe 的妙招在于证明：无论删去的是哪个构形，总能通过交换图中的颜色，使得把删去的顶点加回来时，所有顶点依然可以只用四种颜色着色，无需第五种颜色。

只要证明每个不可避免构形都能以这种方式“可约化”，就等于证明了极小图其实可以四着色——最初的反证假设不成立，四色定理必然成立。

可惜的是，Kempe 宣布证明 11 年后，数学家 Percy John Heawood 在他的颜色交换步骤中发现了一个微妙的漏洞：当删去的顶点恰好有五个邻居时，Kempe 的方法可能导致相同的颜色相邻。Heawood 起初不太愿意指出这个错误，部分原因是 Kempe 的方法实在太优雅了。事实上，尽管有这个错误，Kempe 的交换步骤——如今被称为 Kempe 链——依然成为后来所有证明的核心。“犯了一个错误，结果这错误有趣到以你的名字命名，是不是很有意思？”Thomassen 说。

最终，没有人能证明 Kempe 不可避免集中最后一个构形是可约化的。事实证明，正确的证明需要找出一个庞大复杂得多的集合——包含 8900 个构形——并逐一证明它们都可约化。这项任务靠人力无法完成，必须借助计算机。

1976 年，数学家 Kenneth Appel 和 Wolfgang Haken 想出一个巧妙的办法，首先将需要检查的情形数量降低到 1,936 种，随后进一步降至 1,482 种。接着，他们借助伊利诺伊大学的超级计算机逐一验证了所有这些情形。终于，四色定理得证。

翻译说明：这里原文是 "A student of mine asked me today to give him a reason for a fact which I did not know was a fact — and do not yet,"。意思是学生问了一个事实的理由，但这个事实他原本不知道，现在也不知道。 Wait, let's re-read the De Morgan quote in the source text provided: “A student of mine asked me today to give him a reason for a fact which I did not know was a fact — and do not yet,” he wrote in an 1852 letter... Correction: The source text says: “A student of mine asked me today to give him a reason for a fact which I did not know was a fact — and do not yet,” Actually, looking at the provided text: `“A student of mine asked me today to give him a reason for a fact which I did not know was a fact — and do not yet,” he wrote in an 1852 letter to the prolific mathematician and physicist William Hamilton.` My translation: “今天，我的一位学生要求我解释一个我此前并不知晓的事实——而直到现在我仍一无所知。” This is a bit clunky. Better: “今天，一位学生让我解释某个事实的依据，但我此前并不知道这是个事实——现在依然如此。” Let's re-evaluate the whole block. Original: `They met a skeptical audience. Computers at the time were scary, technically unknowable. Appel and Haken were using core memory, storing information on magnetic material that was hand-woven into a mesh of wires. “There were all kinds of arguments about how you can possibly trust this proof,” said Ellen Gethner, a mathematician at the University of Colorado, Denver. “What happens if there’s a surge of electricity and you miss that one configuration that would have invalidated the proof?”` Translation: 他们面对的听众充满质疑。那时的计算机令人望而生畏，技术细节深不可测。Appel 和 Haken 使用的是核心存储器，信息存储在手织磁芯网格中。“当时有很多争论，大家根本不敢信任这种证明方式，”丹佛分校数学家 Ellen Gethner 说，“如果发生电压波动，恰好漏掉了那个能推翻证明的关键情形，怎么办？” Original: `Still, most people grew to eventually accept that “four colors suffice,” as the University of Illinois later announced on their postal meter stamps. And in 1997, a team of mathematicians put the matter to bed by simplifying Appel and Haken’s approach, using a computer to identify and check just 633 configurations. This time, the mathematical community accepted the result immediately.` Translation: 不过，大多数人最终接受了“四色足够”的结论，正如伊利诺伊大学后来在邮资计票机邮票上宣布的那样。1997 年，一支数学家团队通过简化 Appel 和 Haken 的方法，利用计算机识别并核查了仅 633 种情形，彻底解决了这一争议。这一次，数学界立刻接受了这一结果。 Original: `But the story was far from over.` Translation: 但故事远未结束。 Original: `

Searching No-Man’s Land

` Translation: `

探索无人区

` (or "蛮荒之地", "无人之境") Original: `

The latest chapter started on a Danish beach in 2015.

` Translation: 最新的一幕始于 2015 年丹麦的一处海滩。 Now combine and refine. Final check on the De Morgan caption: Original: “A student of mine asked me today to give him a reason for a fact which I did not know was a fact — and do not yet,” Literal: "A student of mine asked me today to give him a reason for a fact which I did not know was a fact - and do not yet [know it to be a fact]" My draft: “今天，我的一位学生要求我解释一个我此前并不知晓的事实——而直到现在我仍一无所知。” Refined: “今天，我的一个学生让我解释某个事实的依据，但我此前并不知晓这是个事实——现在依然如此。” Let's output.

日本国立信息学研究所（NII）的图论专家川濑賢一（Ken-ichi Kawarabayashi）正在参加一场会议，他的长期合作者 Thorup 也在场。两人刚刚共同发表了一篇重要论文（这篇论文后来为他们赢得了 prestigious 的 Fulkerson Prize，该奖项在数十年前也曾授予 Appel 和 Haken 以表彰他们在四色问题上的工作）。此刻，他们站在 Nyborg 的白色沙滩上，正思索下一步该做什么。“我们没办法真正去做一个小项目，”川濑回忆道，当时他是这么想的。

四色定理对他们的职业生涯产生了巨大影响。一定程度上，正是它激发了他们投身图论研究的兴趣。然而，他们对 1997 年那个成果的一个方面仍感不满：该结果给出了用四种颜色为任意图着色的算法，但这个算法效率低下。对于一个有 n 个顶点的图，着色过程需要 n² 步。

问题在于，如果你拿到一张大图的并希望给它着色，你就得在图中搜索一种构型，移除它，然后搜索另一种构型，移除那个，如此循环——直到把图简化到明显可以被四色着色的状态为止。

点击观看此视频即表示您同意我们的 隐私政策。

川濑和 Thorup，以及不久后加入的 Thomassen 和西蒙弗雷泽大学（Simon Fraser University）的 Bojan Mohar，希望找到一组不可避免的构型，以便并行缩减，而非逐一处理。为此，他们必须保证在缩减每个构型时，不会干扰同时被缩减的其他构型的着色。这将为他们提供一种更快的方式来仅用四种颜色重新为图着色。

如何找到这些互不干扰的构型？方法就是广泛搜索。

在1976年和1997年的四色定理证明中，数学家们只关注那些顶点连接稀少的顶点簇区域。Kawarabayashi、Mohar、Thomassen 和 Thorup 则把目光转向了图中所谓的“平坦”区域——那里每个顶点都与另外六个顶点相连，边构成三角形排列。这类区域堪称图论中的“无人区”：由于平坦区域缺少通常用来证明构型可约性的结构，很难在其中找到好的构型。但研究者们意识到，平坦区域其实要常见得多。而要同时对大量构型进行约化和重新着色、又互不干扰，就需要足够多的候选项可供挑选。

要在这些区域里搜索构型，还需要两双手——Kawarabayashi 的研究生 Yuta Inoue 和 Atsuyuki Miyashita——以及数月的计算时间。“我们当时太天真了，”Thorup 说，“没想到会花这么久。”但最终，他们找到了一个新的不可避免集。这个集合非常庞大，包含 8202 个构型。不过正如他们所希望的，在给定图中可以同时约化其中许多构型，把原来需要很多步的操作压缩到寥寥几步。

四色定理再次得到证明。而且新证明还带来了一套效率高得多的着色算法：对一个有 n 个顶点的图，只需 n(log n) 步，相比原来的 n² 是显著改进。

新视野

正如一个多世纪前肯普失败的尝试一样，新证明的最大价值不在于其轰动性结果，而在于它对图论本质提供的新洞察。通过借鉴不同的可归约性概念并利用图中被忽视的部分，这项研究揭示了这些重要数学对象中先前未知的结构，并为数学家提供了理解它们的新工具。盖斯纳说：“一旦建立起这套机制，你就能发现自己能解决哪类问题。”

例如，图论学家不仅关注平面图，还关注位于各类曲面（如甜甜圈形状的环面）上的图。这些图拥有一些与新研究中在平面图上发现的相似性质，使得关于它们的着色定理也能得以证明。最新四色定理成果的研究者们正在利用他们的技术来解决这些问题。尽管障碍依然存在，但托马森表示：“我认为我们找到了正确的路径。”

与此同时，“四色症候”依然挥之不去。尽管托马森对自己的最新成果感到满意，但他仍然面临着困扰业余爱好者和专业人士长达150年的那个问题：是否有一个更简单的解释来说明为什么任何平面图只需要四种颜色？那个传说中的单页证明，那个能让所有人恍然大悟的理论突破？

托马森说：“我想要一个不依赖计算机的证明。我会永远思考这个问题。”