尽管肯普的证明未能成功，但他提出的“肯普链换色法”成为后续可约构形证明的核心工具。希伍德在指出漏洞的同时，利用该方法成功证明了五色定理，即任意平面图的顶点色数不超过5，这也从侧面印证了肯普方法的合理性与价值 。
3.2 五色定理：四色猜想的“近亲”与过渡
五色定理的证明是四色猜想研究的重要里程碑，它不仅验证了肯普方法的有效性，也为四色猜想的最终证明提供了思路借鉴。希伍德的五色定理证明同样基于数学归纳法，其核心逻辑与肯普的方法一脉相承，但在处理5度顶点时进行了更严谨的修正 。
五色定理的证明步骤如下：
1. 基础情形：V≤5时，显然可用五种颜色着色，成立。
2. 归纳假设：假设所有V=k（k≥5）的平面图都是五色可染的，证明V=k+1的平面图也五色可染。
3. 不可免集应用：V=k+1的平面图中存在度数≤5的顶点v，删除v后得到的图G可五色染。
4. 恢复v的着色：
- 若v的度数≤4，与肯普证明的情况一致，可染为相邻顶点未使用的颜色；
- 若v的度数=5，设相邻顶点为v?-v?，若其中存在同色顶点，v可染为该颜色；若五个顶点颜色各不相同（设为红、黄、蓝、绿、黑），则构造红-蓝肯普链：
- 若v?（红）与v?（蓝）不在同一条红-蓝链中，交换v?所在链的颜色，v?变为蓝色，v的相邻顶点中蓝色出现两次，红色空缺，v可染为红色；
- 若v?与v?在同一条红-蓝链中，该链与v形成回路，将v?（黄）、v?（绿）、v?（黑）分隔，此时构造黄-绿肯普链，v?与v?必不在同一条链中（因被红-蓝回路分隔），交换v?所在链的颜色，v?变为绿色，v的相邻顶点中绿色出现两次，黄色空缺，v可染为黄色。
五色定理的成功证明表明，通过肯普链换色法可以处理5度顶点的大部分情况，而四色猜想的关键难点在于，如何在仅使用四种颜色的前提下，覆盖所有5度顶点的邻接结构。这一区别也揭示了四色猜想的核心挑战：四种颜色的约束使得换色操作的容错率大幅降低，需要穷尽所有可能的邻接结构并证明其可约性 。
3.3 可约构形的拓展：从人工到机器的接力
肯普和希伍德之后，数学家们意识到，四色猜想的证明需要构建一个包含更多构形的不可免完备集——除了单个的1-5度顶点，还需要考虑这些顶点与其相邻区域组成的复杂局部结构。1919年，伯克霍夫首次突破了单一顶点构形的局限，证明了“含有环形区域的构形”是可约的，这一成果启发了后续的构形研究方向：通过增加构形的复杂度，扩大可约构形的覆盖范围 。
在随后的半个多世纪里，数学家们陆续发现了数千种可约构形，但手动验证构形的可约性面临巨大挑战：每个构形的验证都需要复杂的换色链分析和逻辑推理，且随着构形复杂度的增加，人工计算极易出错。到20世纪60年代，尽管可约构形的数量已相当可观，但仍未形成覆盖所有情况的不可免完备集，四色猜想的证明陷入了“构形爆炸”的困境——需要验证的构形数量远超人工处理能力。
此时，计算机技术的发展为解决这一困境提供了可能。1967年，美国伊利诺伊大学的数学家肯尼斯·阿佩尔（Keh Appel）和沃夫冈·哈肯（wolfgang haken）开始合作，将四色猜想的证明转化为计算机可处理的算法问题。他们的核心思路是：
1. 构形生成：基于伯克霍夫的方法，通过“放电法”（一种模拟电荷分配的算法）自动生成可能的不可免构形。放电法的原理是给平面图的每个顶点分配“电荷”，然后根据顶点度数重新分配电荷，最终电荷为正的顶点及其邻域即为不可免构形。
2. 可约性验证：编写程序验证每个生成构形的可约性——通过计算机模拟换色链操作，判断该构形是否能被四色染。
3. 完备性检验：不断迭代生成构形并验证，直至形成一个完整的不可免完备集（即所有平面图都必含该集中的构形）。
这一过程异常艰巨：阿佩尔和哈肯团队需要处理海量的构形数据，优化算法以减少计算量，同时解决程序逻辑错误导致的验证偏差。经过近十年的努力，他们终于在1976年完成了关键突破：生成了包含1936个可约构形的不可免完备集，并通过三台Ibm 360计算机连续运行1200小时，完成了所有构形的可约性验证——近百亿次逻辑判断无一矛盾，四色猜想终于被证明，正式成为“四色定理” 。
3.4 证明的简化与验证：从1