1852年。地圖染色工作中形成的“四色猜想”，多年來一直困擾着數學家。粗看上去。證明“四色猜想”似乎並不困難，可是。細想起來，問題並不簡單。
為什么？
長期以來，使用傳統數學語言（術語與概念）說不清楚四色猜想問題到底屬於什么數學分支。用什么語言表述，連問題本身都說不清楚，更談不上什么“數學證明”了。對此，聰明的數學家也無可奈何，沒有辦法。
一百多年之后，1976年6月。在美國伊利諾斯大學的兩個“小毛頭阿沛爾與哈肯（Appel andHaken）利用兩台計算機與不同檢驗程序，連續執行了一千多小時（近兩個月），直接檢查了一百多億張”人造地圖“（待檢驗地圖），發現根本不須要五種以上的顏色給地圖上色，從而得出不可避免的”結論“：地圖上色。四種顏色就足夠了。
起初，數學家並不承認這樣的利用計算機的”惡搞方法“算是嚴肅的數學證明。
實際上，阿沛爾與哈肯利用計算機證明四色猜想為數學證明開辟了一條新的途徑。也開闊了人們的眼界。使傳統數學證明方法不再是唯一的“正統”。
進入本世紀，2005年，人工智能專家Georges Gonthier利使用方法國國家大型計算機給出了“四色猜想”的“fully checked formal proof”（全檢驗正規證明）。至此，四色猜想最終成為“四色定理”了。嗚呼！
袁萌 7月2日