1852年，地图染色工作中形成的“四色猜想”，多年来一直困扰着数学家。粗看上去，证明“四色猜想”似乎并不困难，但是，细想起来，问题并不简单。为什么？

     长期以来，使用传统数学语言（术语与概念）说不清楚四色猜想问题究竟属于什么数学分支，用什么语言表述，连问题本身都说不清楚，更谈不上什么“数学证明”了。对此，聪明的数学家也无可奈何，没有办法。

    一百多年之后，1976年6月，在美国伊利诺斯大学的两个“小毛头阿沛尔与哈肯（Appel and Haken）利用两台计算机与不同检验程序，连续运行了一千多小时（近两个月），直接检查了一百多亿张”人造地图“（待检验地图），发现根本不需要五种以上的颜色给地图上色，从而得出不可避免的”结论“：地图上色，四种颜色就足够了。起初，数学家并不承认这种利用计算机的”恶搞方法“算是严肃的数学证明。

     实际上，阿沛尔与哈肯利用计算机证明四色猜想为数学证明开辟了一条新的途径，也开阔了人们的眼界，使传统数学证明方法不再是唯一的“正统”。

     进入本世纪，2005年，人工智能专家Georges Gonthier利用法国国家大型计算机给出了“四色猜想”的“fully checked formal proof”（全检验正规证明），至此，四色猜想终于成为“四色定理”了。呜呼！

袁萌 7月2日