1852 年，大学毕业于伦敦院校的弗南西斯·格思里赶到一家科研机构搞地图上色工作中时，发觉了一个趣味的状况：“每一幅地图能够用四种颜色上色，促使有相互界限的国家着上不一样的颜色。”很多年来一直困惑着物理学家。粗看起来。证明“四色猜想”好像并不是艰难，但是。深入细致起來，难题并不容易。

为何？

一直以来，应用传统式数学言语（专业术语与定义）说不清四色猜想难题究竟归属于哪些数学支系。用哪种言语描述，连难题自身都说不清，更算不上哪些“数学证明”了。对于，聪慧的物理学家也万般无奈，沒有方法。

一百多年以后，1976年6月。在国外伊利诺斯高校的2个“小毛头阿沛尔与哈肯（Appel andHaken）运用两部电脑与不一样检测程序流程，持续实行了一千多钟头（近两月），立即查验了一百多亿张”人工合成地图“（待检测地图），发觉本质不需用五种左右的颜色给地图着色，进而算出难以避免的”依据“：地图着色。四种颜色就充足了。

最初，物理学家并不是认可那样的利用软件的”搞怪方式 “算作严肃认真的数学证明。

事实上，阿沛尔与哈肯利用软件证明四色猜想为数学证明开拓了一条新的方式。也开扩了大家的见识。使传统式数学证明方式 已不是唯一的“正统”。

进到21世纪，2005年，人工智能技术权威专家Georges Gonthier利使用说明国国家大型计算机得出了“四色猜想”的“fully checked formal proof”（全检测靠谱证明）。到此，四色猜想最后变成“四色定理”了。