想必你一定听说过四色定理，这个最初源于给地图上国家上色的有趣问题被誉为世界近代三大数学问题之一。数学家用了100多年的时间才给出了真正的证明，所用的计算机证明也登上了数学舞台。如今，在图论领域，还有许多由四色定理衍生出来的有趣问题。例如，一个起源于收音机广播电台的问题：在一个无限大的网格纸上填入数字，同一个数字之间的“距离”必须大于这个数字本身，那么最少需要多少个数字能覆盖整个平面？
年幼的你会对着书房墙面上的世界地图发呆吗？凝视着那五颜六色的图案，畅想着自己将来有一天能够环游世界。而在19世纪的英国，一个古老且经典的数学问题——着色问题，就诞生于这样一份凝视。
故事开始于1852年，英国地图制图师弗朗西斯·古特里在观察地图时提出了一个“给地图着色”的问题。他发现只需要四种颜色就可以对地图进行着色，使得相邻的国家颜色不同。但令他不解的是，这个数字“4”是否是最优的呢？
于是他向他的弟弟弗雷德里克·古特里及其朋友们寻求帮助。在交流中，他们逐渐认识到这个问题与数学有着深刻的联系。于是弗雷德里克向他的老师，伦敦大学学院的数学家奥古斯塔斯·德摩根寻求帮助。德摩根教授尝试之后也无能为力，于是写信将这个问题转交给了他的好友，爱尔兰数学家威廉·哈密顿教授。遗憾的是，充满智慧的哈密顿对这个问题并没有太大的兴趣。
摩尔根在信中写道：“一位学生今天让我说明一个事实，我们不知道它是否可作为一个事实。他说将平面上的一个图形，任意划分成有限个部分并对其每个部分染色，使得相邻部分具有不同的颜色，而且只能用四种颜色。你以为如何？如果这个问题成立，它能引起人们关注吗？”起初，这个“听起来简单易懂的”问题并没有引起数学家们的广泛关注。
直到1878年，英国数学家阿瑟·凯莱在伦敦数学会上正式宣布并命名这一问题为“四色问题”，这才激发了大家的求解欲望。在当时，数学家们普遍认为四色问题不会太难，应该很快就能解决。然而，事与愿违，从“四色猜想”到“四色定理”，经历了漫长的120多年，甚至一度与“费尔马大定理”、“哥德巴赫猜想”同称世界上最著名的三大数学难题。
四色问题的通俗叙述中有很多无效信息，例如每个国家的形状、面积、经纬度等等。
唯一重要的信息便是——相邻（即两个区域共享同一段边界）。忽略掉这些无效信息，我们来看看如何用抽象的图论语言来严格定义这个问题。给定一个图G=(V, E)，其中非空集合V是顶点（vertex）集，E是边（edge）集。这其实要用到对偶图的概念，也就是说，用一个顶点ν∈V来表示地图上的一个国家；用一条边e12=(ν1, ν2)∈E来表示两个顶点（国家）ν1, ν2是相邻的。
下文我们只考虑简单无向图——图的边是无向的，即e12=e21；没有重复边，即连接顶点ν1, ν2的边最多只有一条；没有自环，即不存在只连接一个顶点的边。
于是四色问题便抽象成了一个猜想：对一个简单无向图G=(V, E)的顶点进行着色，使相邻的点颜色不同，那么最少只需要4种颜色。这这里最少所需的颜色数我们称之为——色数（chromatic number）。
起初人们只能通过手工计算，得出对于一个包含了96个国家的地图，四色猜想成立。故事的转折点发生在1879年，一位英国律师阿福瑞德·肯普为四色猜想的证明提供了重要的思路。肯普提出，任何一个简单无向图G=(V, E)中至少有一个顶点具有2、3、4或5个相邻顶点（一个国家至少有2、3、4或5个邻国）。这个命题其实是欧拉公式的应用。假设图G=(V, E)中有ν个顶点、e个边和f个面。
首先任何一个面至少有三条边，两个相邻的面共用一条边，每条边上有2个顶点，因此2e=3f。如果每个顶点都有至少6条边，那么2e≥6ν。但欧拉公式告诉我们，ν-e+f=2。这就推出了一个矛盾。
肯普将上述最多具有5个相邻点的顶点及其相应的边命名为“不可避免的构型”。接下来他利用归纳法，移除掉这个顶点以及相邻的边，得到一个子图G'。
如果这个子图G'满足四色猜想，那么称原图G'是可约的，同时将移除掉的顶点及其边称为“可约构型”。肯普认为，只要能证明所有不可避免的构型都是可约构型（也就是说移除掉对应的顶点及其边后可以四色），那么四色猜想必然成立。用数学的语言讲，假设包含n个顶点的图满足四色猜想，那么对于n+1个顶点的图，必有一个顶点及其边是不可避免构型。
如果相邻点是三色的，那么给移除掉的点涂上第四种颜色，结论自然成立；否则，需要对原图重新涂色，争取释放这个顶点，使它的相邻点可以三色，为此肯普设计了“肯普链”的方法。
然而，在肯普的结果公布11年后，人们发现了其中有一个致命的、无法修复的错误。但肯普的思路依然为后世提供了重要的突破口，人们延续他的方法陆续证明了22国、39国、52国以下的地图可以四色。
直到1976年，美国数学家肯尼斯·阿佩尔与沃尔夫格·哈肯在美国伊利诺伊大学的两台计算机上，耗时1200个小时，终于完成了四色定理的证明。他们延续并改进了肯普的方法，将所有的1936个不可避免构型完全罗列出来，并依次对其验证了可约性。这项工作轰动了世界，不仅仅是因为他们证明一个数学难题，更重要的是这告诉人们计算机也能用于数学的逻辑证明。
在两位数学家将研究成果公之于世的当天，当地邮局为了庆祝，在所有邮件上都加盖了“四色足够”的特制邮戳。
事实上，阿佩尔与哈肯并不是最早意识到要用计算机辅助解决四色猜想的人。早在1950年，德国数学家亨利·希许就曾预测，只有借助于能处理巨量数据的强大计算装置才能对四色猜想中的有限但是数量巨大的不同构型进行检验。在计算机技术还未蓬勃兴起的年代，希许的思想十分超前。他是第一个提倡并试图利用计算机来攻克四色问题的数学家，同时他也慷慨地将自己的许多想法与哈肯交流，可以说他对四色猜想的证明起到了极大的推动作用。
尽管阿佩尔与哈肯的研究成果轰动一时，但在当时并没有得到广泛的认可。人们的质疑主要源于对于计算机证明数学问题的不认可。怀疑者们认为阿佩尔与哈肯的方法本质上是一种穷举检验法，他们只是用机器检验了千万种情况，他们的证明细节隐藏在计算机内，人力是无法进行复核的。数学界呼吁给出一份纯粹明了的数学证明。
30年后来自英国剑桥大学的年轻数学家乔治·贡帝埃给出四色定理的完全计算机化证明，和阿佩尔、哈肯不同的是，他的每一步逻辑证明都由计算机独立完成。经过多年的计算机革命，人们逐渐认可了计算机对于数学工作的帮助，也终于愿意承认——四色定理成立！
数学家们在研究四色猜想的过程中，对其他相关的染色问题也进行了思考。例如最著名的Hadwiger-Nelson问题：在一张无限大的平面上进行点染色，使得相邻的点颜色不同。我们今天介绍的是四色问题的另一种变形：Packing染色问题，也叫广播染色问题。这个问题最早是由克莱姆森大学教授维恩·戈达德等人提出的，它其实来源于一个非常实际的问题——广播电台的频率分配。
每个广播电台所发出信号的覆盖面积都是有限的，信号越强的电台它的覆盖范围也越广。收音机的调频（FM）波段很窄，我国的民用收音机调频范围为FM87.5-108MHz。如果我国每个省市的广播电台都发出不同频率的信号，显然是不切实际的。而两个同频率的电台只有在相距足够远的情况下，它们的信号才不会相互干扰。
那么如何对不同地区广播电台的频率进行分配，使得我们可以在避免干扰的前提下，用最短的信号波段区间来覆盖全国的广播系统呢？数学家们又是如何用数学的语言来定义这件事呢？
与四色定理类似，给定一个简单无向图G=(V, E)，我们用一个整数集合K={1,…,k}来表示颜色集，用d(u, ν)来定义两个顶点u, ν之间的距离。
考虑映射f:V→{1,…,k}，它满足对任意两个顶点u, ν∈V，以及任意的整数c∈K，如果f(u)=f(ν)=c（即顶点u和ν的颜色相同），那么u, ν之间的距离d(u, ν)>c（也就是说具有相同颜色的两个顶点距离足够远；考虑上文的实际背景，这意味着信号频率相同的广播电台距离足够远）。
这样的映射f就构成了一个packing k-染色方案，能满足packing染色方案的最小整数就称为图的packing染色数（packing coloring number）χρ(G)。
packing染色问题其实是在地图着色问题上加了更强的限制。当K={1}时，packing 1-染色问题就是最原始的地图着色问题，即要求相邻两个顶点颜色不同。
我们先来看一个简单的例子，考虑下图中的一维整数轴，取图G=Z={0, ±1, ±2,……}为整数集，每个整数代表一个顶点，两个相邻的整数记为两个相邻的顶点，两个整数之间的距离定义为他们差值的绝对值。构造映射如下：因此d(-2, 2)=4>3=f(-2)=f(2)。那么此时χρ(Z)=3。
上面的例子仅仅考虑了一维情形，如果我们考虑二维平面整数集Z2的染色问题呢？
可以想象，对于一个无限大的平面，我们可以把平面划分成一个个网格（就像一个无限大的棋盘一样），定义两个网格之间的距离为它们之间的水平距离加上垂直距离，那么如何对它们进行packing染色？2008年，戈达德和他的四位合作者首先公开了他们对于这个问题的思考，他们完全用人工计算，得出9≤χρ(Z2)≤23；此后又有几位数学家利用计算机辅助证明，逐步将结果优化为13≤χρ(Z2)≤15。
2022年，来自卡耐基梅隆大学的研究生苏威卡塞乌斯和教授马金·海勒两人将这个结果进一步优化为14≤χρ(Z2)≤15。2023年1月，他们宣布彻底解决了平面整数集Z2的packing染色问题——他们在文章中证明χρ(Z2)=15，即只用1-15这15个数字就能填充整个平面网格，并保证两个具有相同数字的网格之间的距离大于这个数字。下文我们就来简单介绍一下他们的思路和方法。
显然，对一个无限网格用穷举法是不现实也不必要的。所以，数学家想到对其中的一小部分进行验证，比如取一个10×10的网格，后将其复制拼接，如果依然能够满足对距离的要求，即可得证。
苏威卡塞乌斯和海勒首先从这个角度对图进行了简化，但他们并不是考虑简单的矩形，而是从一个类似于菱形的有限子图Dr(ν)={u∈Z2/d(u, ν)≤r}出发，用Dr,k表示对子图Dr[(0, 0)]进行k-packing染色，Dr,k,c表示对子图Dr[(0, 0)]进行k-packing染色而且中心点(0, 0)赋予颜色c。
如果对于子图Dr(ν)可以进行k-packing染色，那么一定有χρ(Z2)≥k；反之χρ(Z2)≥k+1。不难想象，在Dr(ν)这样的有限图中，数字越小出现的次数也就越多；所以在染色过程中可以优先考虑更大的数字的存放位置。比如当r≤k时，子图Dr,k,r中数字r只会在中心点(0, 0)出现一次，否则就会破坏我们对于距离的要求。这也是Dr(ν)相较于矩形子图的优势。
Dr(ν)其实是一个正四边形，具有很好的对称性，因此苏威卡塞乌斯和海勒把Dr(ν)进行八等分，在染色时依次把较大的数字放在1/8角域里进行排列，这样就避免了对染色方案的重复验证。苏威卡塞乌斯和海勒所做的第二个简化是不再单纯地以格点为一个染色单位。他们在Dr(ν)中选取五个相邻的格点，构成一个加号型区域，以这样的加号型区域为一个单位进行染色。
也就是说，可以只考虑把某个数字填入这个加号型区域，但暂时不考虑具体放在这个加号型区域的哪个格点。在排列好加号型区域的染色方案后，再对每个格点进行染色。
正如同行所评价的：苏威卡塞乌斯和海勒不只是在解决问题，他们更是在优化组合学的研究思路。在不懈的努力下，历时四个月，他们最终攻克了平面packing染色问题。
四色定理困扰了数学界一个多世纪，时至今日也没有找到真正纯粹的数学证明。但四色问题的意义已远超这个问题本身，更重要的是在一代代数学家们前赴后继思考的过程中，所衍生出来的对于其他学科分支的思考，例如图论、拓扑、计算机科学等。人们愿意研究四色问题，并不是为了真的用四种颜色填补地图，而是为了探讨“4”这个数字所体现出来的拓扑性质和数学内涵。
作为第一个由计算机辅助证明的数学定理，四色定理由最初的饱受质疑到广泛认可，这注定了它在数学史上的非凡地位。在人工智能飞速发展的今天，AI辅助数学证明成为了大多数学者关注的对象。尽管依然有人认为AI的形式化证明会破坏数学原始的美感，但不可否认的是先进的技术手段确实大幅度地简化了数学家的工作。或许我们应该质疑的并不是计算机本身，而是学者们使用计算机的态度和方法。