四色定理又称四色猜想，由英国绘图员佛朗西斯·格思里（F.Guthrie）在1852年提出。其内容是：“任何一张地图只用四种颜色就能使具有共同边界的国家着上不同的颜色”。许多数学家包括著名的数学家哈密顿（W.R.Hamilton）、闵可夫斯基（H.Minkowski）为之奋斗了100多年都没有解决。直到1976年9月，美国伊利诺斯大学的数学家阿沛尔（K. Appel）和哈肯（W. Haken）教授，在每秒运行400万次的计算机上运行了1200小时，终于证明了四色定理。这是人类第一次利用计算机辅助证明证明了定理。