知识/定理
阿佩尔与哈肯（1976）用计算机证明四色定理：任意平面地图可四色着色。
公式
平面图 $G$ ⇒ $\chi(G)\le4$；「可约构型 + 不可免集」。
证明思路
（计算机辅助）程序检验约 1900 个不可约构型 + 放电法归约——首个主要计算机证明。
应用/例子
图论着色、调度、地图设色、寄存器分配。
意义/影响
计算机证明的开山之作；引发「计算机证明是否算证明」的大辩论。
DOXA · 数学编年史 · 知识详情
1976 ｜ 阿佩尔/哈肯 ｜ 离散·组合 ｜ 突破
阿佩尔与哈肯（1976）用计算机证明四色定理：任意平面地图可四色着色。
平面图 $G$ ⇒ $\chi(G)\le4$；「可约构型 + 不可免集」。
（计算机辅助）程序检验约 1900 个不可约构型 + 放电法归约——首个主要计算机证明。
图论着色、调度、地图设色、寄存器分配。
计算机证明的开山之作；引发「计算机证明是否算证明」的大辩论。