四色定理的证明（计算机辅助）
1976年阿佩尔与哈肯借助计算机完成四色定理证明，首例重大计算机辅助证明。
背景
四色猜想声称：任何平面地图都只需四种颜色，即可使任意两个相邻区域颜色不同。它于1852年由弗朗西斯·格斯里（Francis Guthrie）提出，长期作为组合数学中最著名的未解问题之一。
详细描述
1976年，美国数学家肯尼思·阿佩尔（Kenneth Appel）与沃尔夫冈·哈肯（Wolfgang Haken）在伊利诺伊大学宣布证明四色定理。其核心思路是”不可避免集”与”可约性”的放电法（discharging）：
- 他们将问题转化为：若四色定理不成立，则存在一个”最小反例”地图；通过放电论证可证明，任何最小反例必含约1936种（后经修订）特定”构型”之一。
- 对每一种构型，需验证它是”可约的”（即该构型出现时必能四色）。这一验证涉及海量组合情况，借助计算机完成归约计算。
这是数学史上首个依赖计算机完成的重大证明。
求解过程 / 影响（含最新进展若相关）
该证明当年引发关于”什么才算是证明”的激烈讨论——当正确性依赖人类无法直接复核的机器计算时，证明的可信度如何？其后，罗伯逊（Neil Robertson）、桑德斯（Daniel Sanders）、西摩（Paul Seymour）与托马斯（Robin Thomas）于1996年给出更简洁的证明，仍借助计算机，但构型数大幅减少。四色定理如今是组合图论经典结论，也持续推动”计算机辅助证明”方法论的发展与反思。