四色定理

四色地图的一个例子

四色定理指出每个可以画出来的无飞地地图都可以用不多於4种颜色来上色，而且没有两个相接的区域会是相同的颜色。被称为相接的两个区域是指他们共有一段边界，而不是共有一个交点。

这一定理最初是由法蘭西斯˙葛斯爾在1853年提出的猜想。很明显，3种颜色不会满足条件，而且也不难证明5种颜色满足条件且绰绰有余（僅使用到歐拉-笛卡爾公式）。但是，直到1977年四色猜想才最终由Kenneth Appel和Wolfgang Haken证明。他们得到了J. Koch在算法工作上的支持。

证明方法将地图上的无限种可能情况歸納为1,936种状态（稍后减少为1,476种），这些状态由電腦一个接一个进行检查，这一工作由不同的程序和電腦进行了獨立的复检。在1996年，Neil Robertson、Daniel Sanders、Paul Seymour和Robin Thomas使用了一种类似的证明方法，检查了633种特殊情况。这一新证明也使用了電腦，如果由人工来检查的话是不切实际的。

四色定理是第一个主要由電腦证明的理论，这一证明并不被所有的数学家接受，因为採用的方法不能由人工直接验证。最终，人们必须对電腦编译的正确性以及运行这一程序的硬件设备充分信任。参见電腦協助證明。

主要是因為此證明缺乏数学应有的規範，以至于有人这样评论“一个好的数学证明应当像一首诗——而这纯粹是一本电话簿！”

雖然四色定理證明了任何地圖可以只用四個顏色著色，但是這個結論對於現實上的應用卻相當有限。現實中的地圖常會出現飞地，即兩個不連通的區域屬於同一個國家的情況（例如美國的阿拉斯加州），而製作地圖時我們仍會要求這兩個區域被塗上同樣的顏色，在這種情況下，四個顏色將會是不夠用的。