内容来源：https://www.quantamagazine.org/the-four-color-theorem-gets-a-rare-new-proof-20260910/

内容总结：

四色定理再添新证：数学家另辟蹊径，为百年难题注入新洞见

四色定理堪称数学史上最富传奇色彩的问题之一：给任意一张地图着色，使相邻区域颜色不同，四种颜色是否足够？这个连孩童都能理解的命题，却让数学家们为之痴迷了一个半世纪。如今，一支由丹麦、加拿大和日本研究者组成的团队，在历经近十年努力后，给出了四色定理的又一个计算机辅助证明。该证明于2026年3月在线发布，并将于11月在计算机科学基础年会上正式报告。新证明虽然在复杂度上超过前人，却在过程中提供了一种远为高效的图着色算法，并揭示了平面图结构性质的新洞见，有望推动图论中诸多其他难题的进展。

从地图到图论：一个半世纪的执念

1852年，数学家弗朗西斯·格思里在给英格兰各郡地图着色时注意到，四种颜色似乎总是够用。他将这一疑问告知同为数学家的弟弟弗雷德里克，后者又将其转达给导师奥古斯塔斯·德·摩根。德·摩根对此产生兴趣，并将问题推向更广泛的学术圈。1879年，数学家阿尔弗雷德·布雷·肯普宣称解决了这一问题，《自然》杂志随即发布新闻稿宣布这一“成就”。

肯普的思路是反证法：假设存在一张无法用四种颜色着色的地图，然后证明这一假设终将导致矛盾。他先将地图转化为“平面图”——每个国家用点表示，相邻国家之间连线。18世纪，瑞士数学家欧拉发现平面图具有诸多有用性质，其中之一便是任何平面图都至少含有一个邻居不超过五个的顶点。肯普据此提出“不可避免集”的概念，并展示了如何通过交换颜色使每种构型“可约”，从而证明四色定理成立。

然而11年后，数学家珀西·约翰·希伍德发现肯普的颜色交换程序存在微妙缺陷：当被移除顶点有五个邻居时，肯普的方法可能导致同色相邻。尽管如此，肯普的交换方法——今称“肯普链”——仍成为此后所有解决方案的核心工具。丹麦技术大学图论学家卡斯滕·托马森感叹：“你犯了一个有趣到以你命名的错误，这难道不有意思吗？”

最终，数学家发现正确证明需要识别一个远为庞大复杂的构型集——多达8900种——并逐一证明其可约性，这已非人力所及。1976年，数学家肯尼斯·阿佩尔和沃尔夫冈·哈肯借助伊利诺伊大学的超级计算机，将构型数逐步缩减至1482种并完成验证，宣称四色定理终获解决。但当时计算机尚属“技术黑箱”，许多数学家对计算机证明的可靠性心存疑虑。科罗拉多大学丹佛分校数学家艾伦·格特纳回忆：“当时各种争论层出不穷——万一电压突增让你漏掉了某个致命构型怎么办？”

尽管如此，“四色足够”逐渐被广泛接受。1997年，一个数学家团队用计算机识别并验证了仅633种构型，简化了阿佩尔和哈肯的方法，这一次数学界立即接受了结果。但故事远未结束。

丹麦海滩上的新起点

新篇章始于2015年丹麦的一片海滩。日本国立情报学研究所图论学家川原研一与长期合作者米克尔·托鲁普在参加一场会议时，站在尼堡的白沙上思考下一个研究方向。四色定理深刻影响了他们的职业生涯，甚至促使他们成为图论学家。但他们对1997年的结果仍有一处不满：该证明给出了用四种颜色着色的方法，但效率低下——对于n个顶点的图，着色过程需要n²步。

川原和托鲁普希望找到一组“不可避免集”，其中的构型可以并行约简而非逐个处理，从而大幅提速。托马森和西蒙弗雷泽大学的博扬·莫哈尔随后加入。他们将目光投向图中所谓的“平坦区域”——每个顶点与其他六个顶点相连，形成三角形边结构。这些区域在传统证明中因缺乏结构而难以识别可约构型，但胜在更为常见，为并行约简提供了充足选择。

搜寻构型的工作又耗费了川原的两名研究生井上雄太和宫下笃之数月计算时间。托鲁普坦言：“我们当时太天真了，完全没想到会花这么久。”最终他们找到了一个包含8202种构型的新不可避免集。尽管规模庞大，但正如所愿，其中许多构型可在给定图中同时约简，将原本繁多的步骤压缩为寥寥几步。新证明给出了更高效的着色算法：n个顶点的图仅需n(log n)步，较n²有显著提升。

新工具，新视野

与一个多世纪前肯普的失败尝试一样，新证明的最大价值不在于其标题性结论，而在于它为图的性质提供了新洞见。通过引入不同的可约性概念并利用图中此前被忽视的部分，这项工作揭示了平面图这一重要数学对象中此前未知的结构，为数学家提供了理解它们的新工具。格特纳说：“一旦你建立起机器，你就会发现能解决什么样的问题。”

例如，图论学家不仅关注平面图，还关注环面等曲面上的图。这些图具有新工作在平面图中揭示的某些相同性质，使得关于它们的着色定理同样可证。最新四色定理背后的研究者正利用他们的技术处理这些问题。托马森表示，尽管障碍仍存，“我认为我们找对了路”。

与此同时，“四色病”仍在蔓延。托马森对近期成果感到满意，但那个困扰业余爱好者和专业人士150年的问题依然挥之不去：是否存在更简单的解释，说明为何四种颜色足以应对任何平面图？那个传说中的一页纸证明，那个能让所有人恍然大悟的理论妙笔？

“我想要的是一个不用计算机的证明，”托马森说，“我永远不会停止思考这件事。”

中文翻译：

四色定理罕见地迎来新证明

引言

有些数学问题在得到解决之后，仍会长久地困扰研究者。一个证明出现了，甚至获得了赞誉，然而不满依然挥之不去。也许论证过于繁复——人们仍在追寻那 elusive 的单页论文——又或者它未能就某件事为何为真给出更深层的理论洞见。无论原因如何，数学家们一次又一次地回到那些本已被视为尘埃落定的问题上。

其中最著名的案例之一便是四色定理，这个问题改变了数学家对自己学科的思考方式。

这个问题陈述起来很简单，理解起来更简单：给定一张连通的地图，能否用四种颜色中的一种为每个区域着色，使得相邻区域不共享同一种颜色？19世纪中叶，这个问题对地图制作者来说不过是个微不足道的小兴趣——他们手头远不止四种颜色可用，也看不出有什么特别理由要限制自己的调色板。但对数学家而言，无论是业余爱好者还是专业人士，这个脑筋急转弯很快变成了一种执念。

第一个声称的证明于1879年公布，盛行了11年后才被证明有误。此后又有更多错误答案接踵而至，来自律师、医生，也有著名图论学家。“我们面对的是一个连孩子都能理解的问题，”丹麦技术大学的图论学家卡斯滕·托马森说，“我认为这正是它成为如此巨大挑战的原因。”

这一定理最终在近一个世纪后得到证明——但用的是当时被视为丑闻的计算机方法，这使数学家们开始质疑，究竟什么才算得上是证明。这个问题的地位一直争论不休，直到1997年，计算机的使用变得更加普遍，一个更简单的计算机辅助证明被发现。

然而即便在今天，“四色病”——用哥本哈根大学计算机科学家米克尔·托鲁普的话说——仍在蔓延。他和托马森都自认是患者。对于如此简单的陈述，必定存在一个更简单的理由来解释它为何为真。或者至少存在一种更高效的证明方式。

经过近十年的努力，托鲁普、托马森以及丹麦、加拿大和日本的四位同事，又产生了该定理的另一个计算机证明。

这个证明——于2026年3月在线发布，并将于11月在年度计算机科学基础会议上展示——在某些方面比其前身更加复杂。“看起来他们在实际执行证明时大量使用了电力，”巴黎Inria的计算机科学家乔治·贡蒂耶说。但在构建论证的过程中，研究者们提供了一种远为高效的地图着色方法。在此过程中，他们揭示了关于重要数学对象——平面图——结构性质的新洞见，为解决图论中许多其他棘手问题开辟了可能。

鉴于这个问题充满错误开端和破灭希望的历史，贡蒂耶说，“能真正看到一次实实在在的成果，真是太酷了。”

计算机化的争议

1852年，数学家弗朗西斯·格思里在为英格兰各郡的地图着色时，注意到他只需要四种颜色。他心想，这是否总是成立？他询问了自己的兄弟弗雷德里克，后者也是一位数学家，弗雷德里克的导师奥古斯都·德·摩根对这个问题的兴趣，并决定将其推广给更广泛的受众。1879年，当一位名叫阿尔弗雷德·布雷·肯普的数学家声称找到了解答时，一份新闻稿在《自然》杂志上宣布了这一成就。

肯普首先假设与他想要证明的命题相反的情况：存在一张无法仅用四种颜色着色的地图。然后他试图表明，这一假设最终会导致矛盾——意味着这样的地图不可能存在。若是如此，所有地图都必然可以用四种颜色着色。

首先，他说，设想你假设中那张不可四着色的地图尽可能“极小”：如果你从中移除任何一个国家，剩下的地图都可以四着色。接下来，通过将地图重绘为所谓的平面图，去除地理和其他无关细节。将每个国家表示为一个点（或顶点），如果两个国家共享边界，则在两点之间画一条线（或边）。你的地图着色问题现在变成了图着色问题，从而可以运用图论的工具。

特别是，18世纪瑞士数学家莱昂哈德·欧拉发现平面图具有许多有用的性质——其中包括保证任何这样的图至少包含一个邻居不超过五个的顶点。这意味着你的图必须至少具有以下六种构型之一，即肯普所称的不可避免集：

而由于你的图是极小的，如果你从中移除这些构型中的任何一个，剩下的图都可以用四种颜色重新着色。肯普的天才之举在于表明，无论你移除哪种构型，你总能找到一种方法交换图中颜色，使得当你把缺失的顶点加回来时，可以为所有顶点着色而不需要第五种颜色。

通过表明每个不可避免构型都以这种方式“可约”，你就证明了你的极小图终究是可以四着色的——你最初的假设是错误的。四色定理必然为真。

不幸的是，在肯普宣布其证明11年后，数学家珀西·约翰·希伍德发现了其颜色交换程序中的一个微妙缺陷：在移除的顶点有五个邻居的情况下，肯普的方法可能导致相同颜色最终相邻。希伍德起初不愿报告这个错误，部分原因是肯普的方法如此优雅。事实上，尽管肯普犯了错误，他的交换程序——今天被称为肯普链——仍将是未来解决方案的核心。“你犯了一个如此有趣的错误，以至于以你的名字命名，这不是很有趣吗？”托马森说。

最终，没有人能够证明肯普不可避免集中的最后一个构型是可约的。事实证明，一个正确的证明反而需要识别一个更大、更复杂的8，900个构型的集合——并证明它们全部可约。这项任务不可能手工完成。它需要计算机。

1976年，数学家肯尼斯·阿佩尔和沃尔夫冈·哈肯想出了一种巧妙的方法，先将可能性数目降至1，936个构型，然后降至1，482个。他们随后使用伊利诺伊大学的超级计算机逐一正确地约简每个构型。他们宣称，四色定理终于尘埃落定。

他们遇到的是怀疑的听众。当时的计算机令人恐惧，技术上不可知。阿佩尔和哈肯使用的是磁芯存储器，将信息存储在手工编织成网状电线的磁性材料上。“关于你怎么可能信任这个证明，有各种各样的争论，”科罗拉多大学丹佛分校的数学家艾伦·格斯纳说。“如果出现电涌，你漏掉了那个本可以推翻证明的构型，那该怎么办？”

尽管如此，大多数人最终还是接受了“四种颜色足够”，正如伊利诺伊大学后来在其邮资计费器印章上宣告的那样。1997年，一个数学家团队通过简化阿佩尔和哈肯的方法，用计算机识别并检验了仅633个构型，为这个问题画上了句号。这一次，数学界立即接受了结果。

但故事远未结束。

搜索无人区

最新的篇章始于2015年丹麦的一片海滩。

日本国立信息学研究所的图论学家河原林健一正在与他的长期合作者托鲁普一起参加一个会议。两人最近共同发表了一篇重要论文（后来为他们赢得了著名的富尔克森奖，该奖在几十年前也曾授予阿佩尔和哈肯以表彰他们的四色工作）。他们现在站在尼堡的白沙上，思考下一步该做什么。“我们不能真的做一个小项目，”河原林回忆当时的想法。

四色定理在他们的整个职业生涯中产生了巨大影响。它部分地激励了他们最初成为图论学家。然而，他们对1997年结果的一个方面仍不满意：它为数学家提供了用四种颜色为任何图着色的配方，但这个配方效率低下。对于一个有n个顶点的图，着色过程需要n²步。

问题在于，如果你拿到一个大图想要着色，你必须搜索其中一个构型，移除它，然后搜索另一个构型，移除它，如此反复——直到你把图约简到明显可以四着色的程度。

河原林和托鲁普，很快加入了托马森和西蒙弗雷泽大学的博扬·莫哈尔，想要识别一个可以并行约简的不可避免构型集，而非逐一约简。要做到这一点，他们必须保证能够约简每个构型而不干扰同时被约简的其他构型的着色。这将为他们提供一种远为快速的仅用四种颜色重新着色图的方法。

如何找到这些互不干扰的构型？通过广泛搜索。

在1976年和1997年的四色定理证明中，数学家只关注那些具有少量连接顶点簇的区域。河原林、莫哈尔、托马森和托鲁普则将注意力转向所谓的图的平坦区域，其中每个顶点与另外六个顶点相连，形成三角形边排列。这些区域形成了一种图形化的无人区：在那里识别好的构型更加困难，因为平坦区域缺乏通常用于证明构型可约性的结构。但研究者们认为，平坦区域也更为常见。而且，要一次约简和重新着色许多构型而不让它们相互干扰，他们需要大量可供选择的选项。

在这些区域中搜索构型又需要两个头脑——河原林的研究生井上雄太和宫下敦之——以及数月的计算时间。“我们当时很天真，”托鲁普说。“我认为我们完全不知道会花这么长时间。”但最终他们找到了一个新的不可避免集。它非常庞大，由8，202个构型组成。但正如他们所希望的，在给定的图中可以同时约简其中许多构型，将曾经需要许多步骤的过程变成了仅仅几步。

四色定理再一次得到了证明。而新的证明给出了一种远为高效的着色算法：对于一个有n个顶点的图，它需要n(log n)步，相比n²是显著的改进。

新视野

与一个多世纪前肯普失败的尝试一样，新证明的最大价值不在于其 headline 结果，而在于它为图的本质提供的新洞见。通过运用不同的可约性概念并利用图中被忽视的部分，这项工作揭示了这些重要数学对象中此前未知的结构——并为数学家提供了理解它们的新工具。“一旦你建立起机制，你就会发现你能解决什么样的问题，”格斯纳说。

例如，图论学家感兴趣的不仅是平面图，还有位于各种曲面上的图，如甜甜圈形状的环面。这些图具有新工作在平面图中揭示的一些相同性质——使得证明关于它们的着色定理也成为可能。最新四色结果背后的研究者们现在正在使用他们的技术来解决这些问题。尽管障碍仍然存在，托马森说，“我认为我们走对了路。”

与此同时，四色病仍在流行。虽然托马森对最近的结果感到满意，但他仍然怀有那个困扰了业余爱好者和专业人士150年的同样问题：是否存在一个更简单的解释来说明为什么四种颜色足以应对任何平面图？那神话般的单页论文，那个能让所有人恍然大悟的理论妙笔？

“我想要的是一个不使用计算机的证明，”托马森说。“我永远不会停止思考这件事。”

英文来源：

The Four-Color Theorem Gets a Rare New Proof
Introduction
Some math problems continue to haunt researchers long after they’ve been solved. A proof emerges, is even celebrated, and yet dissatisfaction lingers. Perhaps the argument is too convoluted — the hunt persists for the elusive one-page paper — or perhaps it fails to give a deeper theoretical insight into why something is true. Whatever the reason, mathematicians return, again and again, to a case that is otherwise considered closed.
One of the most famous such cases is that of the four-color theorem, a problem that transformed how mathematicians think about their subject.
The problem is simple to state, and even simpler to see: Given a contiguous map, is it possible to color each region with one of four colors such that no neighboring regions share a color? In the mid-19th century, the question was of trifling interest to mapmakers, who had far more than four colors at their disposal and saw no particular reason to restrict their palette. But to mathematicians, both amateur and professional, the brain teaser quickly turned into an obsession.
The first purported proof, announced in 1879, stood for 11 years before it was proved incorrect. More wrong answers would follow, from lawyers and doctors and famous graph theorists, too. “Here we have a problem that even a child can understand,” said Carsten Thomassen, a graph theorist at the Technical University of Denmark. “I think that’s the reason why it has been such a big challenge.”
The theorem was finally proved nearly a century later — but with computer methods that were considered scandalous at the time, causing mathematicians to question what they considered a proof in the first place. The status of the problem remained a source of debate until 1997, when the use of computers became more common and a simpler computer-assisted proof was found.
Yet even today, the “four-color disease,” as Mikkel Thorup, a computer scientist at the University of Copenhagen, puts it, continues to circulate. He and Thomassen count themselves among the afflicted. For such a simple statement, there must be a simpler reason why it is true. Or at least a more efficient way to demonstrate it.
After nearly a decade of work, Thorup, Thomassen, and four colleagues in Denmark, Canada, and Japan have produced yet another computer proof of the theorem.
The proof — which was posted online in March 2026 and will be presented in November at the annual Foundations of Computer Science conference — is in some ways even more complicated than its predecessors. “It looks like they’ve used electricity liberally in actually carrying out their proof,” said Georges Gonthier, a computer scientist at Inria in Paris. But in the process of crafting their argument, the researchers provided a far more efficient way to color maps. And in doing so, they uncovered new insights into structural properties of important mathematical objects called planar graphs — opening up the potential for progress on many other stubborn problems in graph theory.
Given the problem’s history of false starts and dashed hopes, Gonthier said, “it’s really cool to see a real result for once.”
Computerized Controversy
In 1852, the mathematician Francis Guthrie was coloring in a map of English counties when he noticed that he needed only four colors. Was this always true, he wondered? He asked his brother Frederick, also a mathematician, whose adviser, Augustus De Morgan, took an interest in the question and decided to market it to a wider audience. In 1879, when a mathematician named Alfred Bray Kempe claimed to have a solution, a press release announced the achievement in Nature.
Kempe started by assuming the opposite of what he wanted to prove: that there is a map that can’t be colored with only four colors. He then sought to show that this assumption would ultimately lead to a contradiction — meaning that no such map could exist. In that case, all maps would have to be four-colorable.
First, he said, imagine that the non-four-colorable map from your assumption is as “minimal” as possible: If you were to remove any country from it, the remaining map would be four-colorable. Next, do away with geography and other extraneous details by redrawing your map as what’s known as a planar graph. Represent each country as a point (or vertex), and draw a line (or edge) between two points if those countries share a border. Your map-coloring problem is now a graph-coloring one, opening it up to the tools of graph theory.
In particular, in the 18th century, the Swiss mathematician Leonhard Euler discovered that planar graphs have many useful properties — among them a guarantee that any such graph will contain at least one vertex with five or fewer neighbors. That means that your graph must have at least one of these six configurations, what Kempe called an unavoidable set:
And because your graph is minimal, if you remove any of these configurations from it, you’ll be left with a graph that can be recolored with four colors. Kempe’s genius move was to show that no matter which of these configurations you remove, you can always find a way to swap the graph’s colors around so that when you add your missing vertex back, it’s possible to color all the vertices without needing a fifth color.
By showing that each unavoidable configuration is “reducible” in this way, you’ve demonstrated that your minimal graph is four-colorable after all — your original assumption was wrong. The four-color theorem must be true.
Unfortunately, 11 years after Kempe announced his proof, the mathematician Percy John Heawood discovered a subtle flaw in his color-swapping procedure: In the case where the vertex you remove has five neighbors, Kempe’s method could lead to the same colors ending up next to one another. Heawood was initially reluctant to report the error, in part because Kempe’s approach was so elegant. And indeed, despite Kempe’s error, his swapping procedure — today known as a Kempe chain — would remain at the core of future solutions to the problem. “Isn’t it interesting that you make a mistake which is so interesting that it’s named after you?” Thomassen said.
In the end, no one was able to show that the last configuration in Kempe’s unavoidable set was reducible. It turned out that a correct proof would instead require identifying a much larger, more complicated set of 8,900 configurations — and showing that all of them are reducible. The task was impossible to deal with by hand. It needed computers.
In 1976, the mathematicians Kenneth Appel and Wolfgang Haken figured out a clever way to lower the number of possibilities first to 1,936 configurations, and then to 1,482. They then used the supercomputers at the University of Illinois to properly reduce each one. At last, they said, the four-color theorem was settled.
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?”
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.
But the story was far from over.
Searching No-Man’s Land
The latest chapter started on a Danish beach in 2015.
Ken-ichi Kawarabayashi, a graph theorist at Japan’s National Institute of Informatics, was at a conference with Thorup, his longtime collaborator. The pair had recently published a major paper together (which would later win them the prestigious Fulkerson Prize, also awarded decades earlier to Appel and Haken for their four-color work). They now stood on the white sand of Nyborg, wondering what to do next. “We can’t really work on a small project,” Kawarabayashi recalled thinking.
The four-color theorem had been a huge influence throughout their careers. It had inspired them, in part, to become graph theorists in the first place. Yet they remained dissatisfied with one aspect of the 1997 result: It had given mathematicians a recipe for coloring any graph with four colors, but that recipe was inefficient. For a graph with n vertices, the coloring process would require n2 steps.
The problem was that if you were handed some large graph and wanted to color it, you would have to search through it for one configuration, remove it, then search for another configuration, remove that, and so on — until you’d reduced your graph to something that was clearly four-colorable.
Kawarabayashi and Thorup, soon joined by Thomassen and Bojan Mohar of Simon Fraser University, wanted to identify an unavoidable set of configurations that could be reduced in parallel, rather than one by one. To do so, they’d have to guarantee that they could reduce each configuration without interfering with the colorings of the other configurations getting reduced at the same time. That would give them a far faster way to recolor a graph with just four colors.
How to find these non-interfering configurations? By searching widely.
In the 1976 and 1997 proofs of the four-color theorem, mathematicians focused only on regions that featured clusters of vertices with few connections. Kawarabayashi, Mohar, Thomassen, and Thorup instead directed their attention to so-called flat areas of the graph, where every vertex is connected to six others, forming a triangular arrangement of edges. These areas form a sort of graphical no-man’s land: It’s harder to identify good configurations there, since flat regions lack the structure that’s usually used to prove a configuration’s reducibility. But, the researchers figured, flat areas are also much more common. And to reduce and recolor many configurations at once without letting them interfere with each other, they’d need a lot of options to choose from.
The search for configurations in these regions would take two more minds — Kawarabayashi’s graduate students, Yuta Inoue and Atsuyuki Miyashita — and months of computing time. “We were pretty naïve,” Thorup said. “I don’t think we had any clue it would take so long.” But eventually they landed on a new unavoidable set. It was massive, consisting of 8,202 configurations. But as they’d hoped, it was possible to reduce many of those configurations at the same time in a given graph, turning what had once been many steps into just a few.
Once again, the four-color theorem had been proved. And the new proof gave a far more efficient coloring algorithm: For a graph with n vertices, it required n(log n) steps, a significant improvement over n2.
New Horizons
As with Kempe’s failed attempt more than a century ago, the greatest value of the new proof lies less with its headline result than with the new insights it provides into the nature of graphs. By drawing on a different concept of reducibility and using overlooked parts of the graph, the work has revealed previously unknown structure in these important mathematical objects — and has given mathematicians new tools for understanding them. “Once you build up machinery, you find out what kind of problems you can solve,” Gethner said.
For instance, graph theorists are interested not just in planar graphs, but in graphs that lie on all sorts of surfaces, such as the doughnut-shaped torus. These graphs have some of the same properties that the new work uncovered in planar graphs — making it possible to prove coloring theorems about them as well. The researchers behind the latest four-color result are now using their techniques to address these questions. Though obstacles remain, Thomassen said, “I think we have the right path.”
Meanwhile, the four-color disease lives on. While Thomassen is pleased with his recent result, he still has the same question that has dogged hobbyists and professionals alike for 150 years: Is there a simpler explanation for why four colors suffice for any planar graph? The mythical one-pager, the theoretical flourish that would make everyone go “aha”?
“What I would like is a proof without the use of a computer,” Thomassen said. “And I will never stop thinking about that.”