问题
四色定理（ «每个平面图 4-可着色 »）的已知证明全部 «计算机助力 »：Appel–Haken 1976（1482 构形）与 Robertson–Sanders–Seymour–Thomas 1995（633 构形）。 «人可读 » 愿景：压缩到 «数十个构形、几页代数 »—— «可约性 » 检查的人类化。
主要概念
放电与可约性机器
证明骨架：①放电（discharging）： «三角剖分 » 的 «低度 » 结构存在（ «极小反例 » 的 «必含 » 构形）；②可约性：每个 «必含 » 构形 «可约 »（ «删-缩-染-还 » 的 «延拓 » 成功）—— «穷举 » 每构形的 «有限 » 情形。 «633 » 的 «压缩 » 空间： «放电 » 的 «权 » 设计与 «构形 » 的 «更大 » 化（ «每个构形 » 覆盖更多 « 反例 »）—— «可读性 » 与 «验证 » 的 «权衡 »。
「自动短证明」路标
«Hadwiger 猜想 k = 5»（ «本册 49 号 » 的 « 真嵌 » 版）： «4-色 ⟹ « K₅ » 子式 » 已证； «⟸»（ «K₅ 子式 ⟹ 4-色 »）的 «直接 » 证明会 «自动 » 给 « 短 » 四色证明—— «结构 » 捷径之一。 «Barnette 猜想 »（22 号）的 «证明 » 同样 «绕 » 开 «633 »（ «Barnette ⟹ « 四色 » 的 « 桥 » 存在）。故 «人可读四色 » 是 «结构图论 » 的 «路标 » 而非 «纯哲学 » 诉求。
主要命题与证明
命题 1（Birkhoff–Lewis 型构形可约，完整骨架） «Birkhoff 菱形 »（ «环 6 » 构形）可约—— «手动 » 可验证的 «最大 » 构形之一（ «六页 » 级验证）： «染色延拓 » 的 «Kempe 链 » 分析。
梗概 «删构形 → 染余图（归纳） → 还原 »： «还原 » 的 «障碍 » 是 «Kempe 链 » 的 «意外交锁 »； «菱形 » 的 «环结构 » 允许 «枚举 » 所有 «边界染色 »（ «有限 » 且 «小 »），逐一 «解链 »。□
命题 2（Hadwiger k = 5 的 « 桥 »） «5-色 ⟸ « K₅ » 子式 »（ «Wagner 等价 »：Hadwiger k=5 ⟺ 四色定理）—— « Wagner 图 » 的 «结构 » 定理把 «等价 » 变 «真 »； «⟸» 的 «独立 » 证明是 «可读 » 路标。
进展与文献
Appel–Haken 1976；Robertson–Sanders–Seymour–Thomas 1995（ «633 »）； «放电 » 的 «新设计 »：Steinberger 的 «更少 » 构形尝试；Gonthier 的 «形式验证 »（Coq 证明 2005—— «机器 » 可信但非 «人可读 »）； «Hadwiger » 与 «Barnette » 的 «路标 » 文献（ «22 号 »、 «49 号 »）。开放核心： «数十构形 » 的 «放电 » 设计（ «构形 » 的 «智能 » 覆盖）； «Kempe 链 » 的 «高阶 » 机器（ «人工 » 可控的 «解链 » 代数）； «形式验证 » 与 «可读 » 的 «桥 »（ «Coq 的 « 结构 » 可否 « 人工 »»）。