在前面章节中，我们讲到肯普先生发现：忽略地图中某个国家的邻国数目为1的情况，最少邻国数目为2﹑3﹑4﹑5的情形可构成地图构形的不可避免集（即对于所有的地图来说，地图中必然有某个国家，其邻国数目只有2个﹑3个﹑4个或者5个）。如下图1中所示：
既然这个不可避免构形集的存在已经被发现，逻辑上讲：只要证明构成此不可避免集的四种地图构形都是可约构形，便足以证明“四色定理”是成立的。对于最少邻国数目为2﹑3﹑4的地图，我们都已成功证明其为可约构形地图；但对于最少邻国数目为5的地图，证明过程就变得异常艰难！
为解决此问题，伯克霍夫的构想是使用反证法：假设存在某些地图，其至少需要5种颜色染色，那么此类地图中的国家数目最少的那张地图便称为“极小五色地图”，此“极小五色地图”必然是“不可约的”。我们只要找到“一组构形”，使“极小五色地图”中不可避免地会出现“这组构形”中的其中一种构形，而“这组构形”中每种构形都是可约的，那么就能够通过约化将地图的国家数减少，这样就得出：必然存在国家数目比“极小五色地图”更少的地图至少需要5种颜色涂染，从而导致与假设相矛盾。
伯克霍夫提出以相邻国家连成的环来将整个地图M分为三个部分：环内部分A、环外部分B以及环本身R。若环上的国家数为n就称其为n-环。如果R的任意染色都不妨碍A进行染色，那么就可以“忽略”A而将M的染色问题约化为B+R的染色问题，这时便称A+R是可约构形，R称为可约环。伯克霍夫证明了：当R是4-环，或者R是5-环且A中国家不止一个，或者A+R是“伯克霍夫菱形”(见下图2)时，A+R都是可约的构形。因此极小五色地图不可能包含这些构形。
而富兰克林证明：极小五色地图中必定包含三个邻接的五边国（5邻国的国家），或者邻接的两个五边国与一个六边国，或者邻接的一个五边国和两个六边国（如下图3中所示）。他从而得出一系列的可约构形，形成了25国以下地图的不可避免的可约构形集。因此推出，极小五色地图必定至少包含26个国家。
尽管科学家们为寻找不可避免集给出了系统的方法，这种方法的终极目标是找到所有地图的不可避免的可约构形集。然而随着国家数增多，要找到不可避免集并证明其可约化性就越难。这主要是因为随着环的增大，染色的方法数目会迅速增大。6-环的染色方法有31种，而12-环则有22144种。因此对大环围成的构形验证可约性是十分繁杂的工作。
为此科学家们又开发出了“放电法”。放电法利用地图转换成图染色后成为平面图的特性，将其看作是平面的“电网”，并将每个“节点”按照度数（连出的边数）分类。首先在每个度数为k的节点放置6 - k的电荷。根据平面图和极小五色地图的特性，有下列恒等式：
其中forall kin {mathbb {Z}},,,A_{k}表示度数为k的节点个数，s为节点最大度数。“放电”的过程指的是将这些电荷以特殊的规则进行重新分配，从而找出“电网”结构上的特性，创建不可避免集。具体来说，可以假设某些构形全不存在，然后构造一个放电过程，使得接受电荷的总量不再等于释放电荷的总量，从而导出矛盾（电荷不守恒）。每个良好设计的放电过程都能证明一个不可避免集的存在。
但人工寻找不可避免构形集和验证构形可约性过于缓慢，数学家开始考虑使用当时新出现的计算机作为辅助，以提高验证的效率。构造出放电法的同时，借助于计算机来验证构形可约性的工作也飞速进展。最先他们使用的是Algol60语言，在一台CDC1504A电脑上运行。但由于内存不足，只能验证12-环以下的构形。而希尔找出的不可避免集含有的大构形可以达到14-环甚至更多，计算机的能力并不足以快速完成可约性的验证。
此时的人们对解决四色问题的前途感到悲观，因为寻找并验证合适的不可避免可约构形集实在过于复杂，即便借助计算机也需要过多的时间。同时人们也认为，即便最乐观的估计中，不可避免集也要包含至少8000个构形。连计算机都难以承受的繁重的验证工作意味着：证明“四色定理”的思路和方式需要进一步调整。在这种需求的推动下，数学家哈肯和阿佩尔依赖于计算机的工作能力，不断改良放电过程。他们将通过放电过程寻找不可避免集的算法和验证可约性结合起来，当某个不可避免集的构形不是C-可约（可约性的一种）或难以被验证为C-可约的时候，就放弃这个不可避免集，以提高效率。
1975年，哈肯找到一种很好的放电过程，但难以化为算法程序。于是两人暂时开始回归纸笔计算。这时候他们得到当时还是博士学生的约翰·科赫支持，后者对他们提供了可约性验证算法工作上的帮助。1976年3月，他们终于得到一个由1936个构形组成的不可避免集，对应的放电过程由487条规则构成。同时伊利诺伊大学的主电脑也更换成运算速度更高的IBM360，为计算节省大量时间。经过电脑1200小时的验证，他们终于在6月得出：1936个构形都是可约构形。这代表着“四色定理”最终的解决。
就这样，困扰人们数百年的数学难题终于被拿下，“四色定理”也成了史上第一个主要由电脑验证成立的著名数学定理。
