人工智能应用- 和数学家做朋友：02. 经典案例：四色定理
在数学中，一些看似简单的定理实际上因需要考虑大量复杂情况而难以手工证明。计算机因其快速运算和精确记忆的优势，成为数学家探索此类难题的有力工具。其中，“四色猜想”的证明就是一个经典案例。四色猜想的内容是：“任意一幅地图都可以用四种颜色完成染色，并确保相邻的区域不会使用相同的颜色。”这一猜想最早由英国制图员弗朗西斯·古斯里（Francis Guthrie）于 1852 年提出。在随后的一个多世纪里，无数数学家试图证明这一猜想，但始终未能成功。
1976 年，数学家肯尼斯·阿佩尔（Kenneth Appel）和沃尔夫冈·哈肯（Wolfgang Haken）利用计算机首次机学家。
图:四色定理示意图
成功证明了四色猜想。他们使用两台计算机，耗时 1200 小时，执行了约 100 亿次推理运算，最终证明了四色猜想的正确性，使其正式成为“四色定理”。这一突破性成果标志着计算机在数学定理证明领域的里程碑。