1852年，地图染色工作中形成的“四色猜想”，多年来一直困扰着数学家。粗看上去，证明“四色猜想”似乎并不困难，但是，细想起来，问题并不简单。为什么？
长期以来，使用传统数学语言（术语与概念）说不清楚四色猜想问题究竟属于什么数学分支，用什么语言表述，连问题本身都说不清楚，更谈不上什么“数学证明”了。对此，聪明的数学家也无可奈何，没有办法。
Appel利用两台计算机与不同检验程序，连续运行了一千多小时（近两个月），直接检查了一百多亿张”人造地图“（待检验地图），发现根本不需要五种以上的颜色给地图上色，，从而得出不可避免的”结论“：地图上色，四种颜色就足够了。起初，数学家并不承认这种利用计算机的”恶搞方法“算是严肃的数学证明。
实际上，阿沛尔与哈肯利用计算机证明四色猜想为数学证明开辟了一条新的途径，也开阔了人们的眼界，使传统数学证明方法不再是唯一的“正统”。
Georges Gonthier
袁萌日
版权声明：本文为博主原创文章，未经博主允许不得转载。
什么天荒地老，什么至死不渝。都只是锦上添花的借口…
