用 Python 演示四色定理证明的核心思想：放电法 + 可归约性 + Kempe 链。
任何平面地图，只需四种颜色，就能使相邻区域颜色各不相同。
1976 年，Appel 与 Haken 借助计算机完成了人类历史上第一个重要定理的计算机辅助证明，共检验 1,936 种不可避免构型。1997 年 Robertson 等人将其简化至 633 种。本项目演示该证明的骨架框架。
欧拉公式 V - E + F = 2
↓
Σ(6 - deg(v)) ≥ 12 > 0 ← 放电法
↓
任意平面图必含"不可避免构型"（度数 ≤ 5 的顶点等）
↓
假设存在最小 4 色反例 G*
↓
G* 必含上述构型 → 该构型可归约（Kempe 链论证） → 矛盾
↓
最小 4 色反例不存在 → 所有平面图均可 4 着色 □
| 概念 | 说明 |
|---|---|
| 放电法 (Discharging) | 给每个顶点赋电荷 6 - deg(v)，由欧拉公式总电荷 ≥ 12 > 0，证明低度数顶点必然存在 |
| Kempe 链 | 颜色 a/b 的交替连通分量；交换链上颜色不破坏合法着色，可为新顶点腾出颜色 |
| 可归约性 | 低度数构型不可能出现在最小反例中：deg ≤ 3 平凡可归约，deg = 4 由 Kempe 链 + 平面性保证，deg = 5 由 Birkhoff 菱形论证（1913） |
Four-Color-Theorem/
├── four_color_appel_haken.py Python 演示程序
├── results/
│ ├── result_1.txt 轮图 W5 的运行结果
│ ├── result_2.txt 3×3 网格的运行结果
│ ├── result_3.txt 十二面体图的运行结果
│ └── result_4.txt 二十面体图的运行结果
└── animation/ 浏览器可视化动画
├── index.html
├── css/style.css
└── js/
├── voronoi.js 像素化 Voronoi 计算（最近邻法）
├── coloring.js 四着色回溯算法 + 轨迹记录
├── scene.js 场景生成（随机多层布点）
├── renderer.js 逐像素渲染
└── main.js 动画主循环与状态机
| 模块 | 功能 |
|---|---|
Graph |
无向图（邻接集），含平面性检测 |
discharging_analysis() |
阶段一：放电法，展示欧拉推导与电荷分配 |
explain_reducibility() |
阶段二：可归约性说明，含 Kempe 链论证文字证明 |
KempeChain |
Kempe 链查找与颜色交换 |
four_color() |
阶段三：最小度优先贪心 + Kempe 链 + 回溯兜底 |
verify_and_print() |
验证着色合法性并输出结果 |
appel_haken_demo() |
主演示框架，串联三个阶段 |
直接用浏览器打开 animation/index.html（无需服务器）。
每一轮随机生成一张由 380–600 个 Voronoi 区域构成的复杂平面图，然后实时演示 Welsh-Powell 排序 + 回溯法 的四着色过程：
- 每次试色（赋颜色）和退色（回溯）都逐步可见
- 全图着色完成后静止展示，随后淡出切换到新图
- 切换期间后台预算下一张，过渡无卡顿
点击或按任意键 可立即跳到下一张。
依赖
pip install networkx运行
python3 four_color_appel_haken.py按提示选择测试图：
1. 轮图 W5 — 简单，含高度数中心顶点
2. 3×3 网格 — 所有顶点 deg ≤ 4，Kempe 链基础演示
3. 十二面体图 — 所有顶点 deg=3，经典案例
4. 二十面体图 — 所有顶点 deg=5，Kempe 链最复杂场景
| 图 | 顶点数 | 边数 | 顶点度数 | 特点 |
|---|---|---|---|---|
| 轮图 W5 | 6 | 10 | 中心 deg=5，外圈 deg=3 | 最简单 |
| 3×3 网格 | 9 | 12 | ≤ 4 | 贪心直接可解 |
| 十二面体图 | 20 | 30 | 全 deg=3 | 经典三正则平面图 |
| 二十面体图 | 12 | 30 | 全 deg=5 | 最具挑战性，充分体现 Kempe 链 |
本程序演示的是证明骨架，与 Appel-Haken 完整证明的差距在于：
- 不可避免构型集：完整证明需检验 1,936 种构型，本程序仅处理度数 ≤ 5 这一族
- 可归约性验证：完整证明对每个构型用计算机穷举验证"D-可归约性"，本程序用 Kempe 链给出教学论证
- 放电规则：完整证明使用数十条精细放电规则，本程序仅展示最基础的两条
完整的形式化验证由 Gonthier（2005）在 Coq 定理证明器中完成，代码约 60,000 行。
- Appel, K. & Haken, W. (1977). Every planar map is four colorable. Illinois Journal of Mathematics, 21(3).
- Robertson, N., Sanders, D., Seymour, P., & Thomas, R. (1997). The four-colour theorem. Journal of Combinatorial Theory, Series B, 70(1), 2–44.
- Gonthier, G. (2008). Formal proof — The four-color theorem. Notices of the AMS, 55(11), 1382–1393.
- Kempe, A. B. (1879). On the geographical problem of the four colours. American Journal of Mathematics, 2(3), 193–200.