颜料青黄蓝褐，

慢把地图勾勒。

疆域必分明，

求证百年无策。

攻克，攻克，

人在机前羞涩。

  相传，四色问题是一名英国绘图员提出来的，此人叫格思里。1852年，他在绘制英国地图的发现，如果给相邻地区涂上不同颜色，那么只要四种颜色就足够了。100年来，无数优秀的数学家企图证明它都以失败告终，四色猜想的证明过程大大促进了拓补学的进展，1936年数学家希奇证明，只要证明10000多种情形下的地图四色猜想成立即可成为定理，但靠笔来算在当时是不可能的。
　　1972年起，黑肯与阿佩尔开始对希奇的方法作重要改进。到1976年，他们认为问题已经压缩到可以用计算机证明的地步了。于是从1月份起，他们就在伊利诺伊大学的IBM360机上分1482种情况检查，历时1200个小时，作了100亿个判断，最终证明了四色定理。在当地的信封上盖“Four colorssutfice”（四色足够了）的邮戳，就是他们想到的一种传播这一惊人消息的别致的方法。
　　人类破天荒第一次运用计算机证明著名数学猜想，应该说是十分轰动的。但说穿了，这种方法其实是“穷举法”，严格来说不能叫“证明”。直到现在为止还没有人能给出严格的逻辑推理证明，所以四色定理的证明，是说人类聪明呢，还是计算机在嘲笑人们愚蠢呢？