四色定理指出，任何画在平面上的地图都可以用至多四种颜色着色，使得任何两个拥有公共边界的区域不会使用同一种颜色。若两个区域只在一个点上接触，它们可以使用同一种颜色。无论地图有多复杂，这个结论都成立。
区域 1、2、3 和 4 都与多个其他区域相邻。左侧的 4 号颜色区域和右侧的 4 号颜色区域并不共享边界，因此可以使用同一种颜色。这个例子恰好需要 4 种颜色。
Francis Guthrie 在 1852 年给英格兰郡县地图着色时提出了这一猜想。他发现四种颜色似乎总是足够，但无法给出证明。这个问题在之后的 124 年里一直难倒数学家。许多错误证明被发表后又被推翻。相比之下，五色定理始终成立，而且可以借助平面图的欧拉公式手工证明。
从最初的猜想到最终证明，历时 124 年。1976 年的证明成为第一个由计算机验证的大型数学定理。
肯尼斯·阿佩尔和沃尔夫冈·哈肯在 1976 年给出的证明，是第一个借助计算机完成的大型数学定理证明。他们把所有可能的地图约化为 1,936 种构型，再让计算机逐一检查，总共耗费 1,200 多小时 CPU 时间。很多数学家对这种无法完全手工核查的证明感到不安。若存在完全人类可读的证明，至今仍未找到。
如果外围有五个区域，也就是奇数个区域，那么这个环本身就必须使用 3 种颜色：5 环不能只用 2 种颜色染色。中央区域与这五个外围区域全部相邻，因此会接触到环上的全部 3 种颜色，于是它必须使用第 4 种颜色。这说明四色有时确实是必要的。
任何画在平面上的地图都可以用不超过四种颜色着色，使任意两个有公共边界的区域不共享同一种颜色。Francis Guthrie 在 1852 年提出这个猜想。Appel 和 Haken 在 1976 年通过计算机检查 1,936 种构型证明了它，使其成为第一个大型计算机辅助证明定理。Robertson、Sanders、Seymour 和 Thomas 在 1997 年把需要检查的构型减少到 633 种。在环面上，这个定理不再成立，那里最多可能需要 7 种颜色。