Correct but Not Explanatory: The Machine Proof of the Four Colour Theorem — Epoche C1
In 1976 Kenneth Appel and Wolfgang Haken announced a proof that every planar map — every division of the plane into regions, like countries on an atlas — can be coloured with four colours so that no two regions sharing a border get the same colour. Their argument reduced the problem to a list of special cases and handed the list to a computer, which worked through it in about 1,200 hours. No human being has ever read the proof in full, and no human being ever will. The objection came at once: a proof that no person can read is not really a proof. This essay argues that the objection runs together two separate complaints — one about reliability, one about explanation — and that the two have met opposite fates. To see why, the argument itself has to be laid out, because both complaints are complaints about its shape. The shape of the proof The strategy is proof by minimal counterexample: assume some planar map needs five colours, take one with the fewest regions, and derive a contradiction from its structure. Three preliminary reductions turn the map into a manageable object. First, replace the map by its graph — one vertex per region, one edge joining two vertices whose regions share a border. Colouring regions becomes colouring vertices so that adjacent ones differ. Second, assume the graph is a triangulation : a planar graph in which every face is bounded by exactly three edges. This costs nothing, because adding edges to a planar graph can only make it harder to colour, and any planar graph can be extended to a triangulation on the same vertices. Third, note that in a minimal counterexample every vertex has at least five neighbours. A vertex $v$ with three or fewer neighbours can be deleted, the smaller graph coloured by minimality, and $v$ given a colour its few neighbours have not used; a vertex with four neighbours needs one extra device, described below, but also goes. So the smallest possible counterexample has minimum degree five. Now count. For any connected planar graph, Euler's formula relates the numbers of vertices $V$, edges $E$ and faces $F$: $$V - E + F = 2.$$ In a triangulation each face has exactly three edges and each edge lies on exactly two faces, so $3F = 2E$, giving $F = 2E/3$; substituting and clearing denominators yields $E = 3V - 6$ exactly — not merely the inequality $E \le 3V - 6$ that holds for planar graphs in general. Exactness matters for what follows. Assign each vertex $v$ a charge of $6 - \deg(v)$, where $\deg(v)$ is its number of neighbours. Since the degrees sum to $2E$, the total charge is $$\sum_v \left(6 - \deg(v)\right) = 6V - 2E = 6V - 2(3V - 6) = 12,$$ exactly twelve, for every triangulation whatever. This is Euler's formula rearranged and nothing more. Because the minimum degree is five, only degree-five vertices carry positive charge, one unit each; every other vertex carries zero or less. So a minimal counterexample must contain at least twelve units' worth of degree-five vertices, no matter how large it is. The discharging step exploits this. Appel and Haken devised rules that move charge from vertices to their neighbours — a degree-five vertex sending a fixed fraction of its charge to certain nearby vertices of high degree, and so on. Moving charge about cannot change the total, which stays at twelve, so after discharging some vertex must still be positively charged. The content of the argument is the case analysis showing what the neighbourhood of such a vertex can look like: if the graph avoided every pattern on a certain finite list, the rules would drain every vertex to zero or below, contradicting the total of twelve. The list therefore has the property that every triangulation of minimum degree five contains at least one member. Such a list is called an unavoidable set , and its members are configurations : a small cluster of vertices together with the ring of neighbours enclosing it. Appel and Haken's set, in the 1977 announcement, had 1,936 members. The second half is reducibility , published as a companion paper with John Koch. A configuration is reducible if it cannot occur in a minimal counterexample. The test runs as follows. Delete the cluster inside the ring; by minimality the rest of the graph has a four-colouring; that colouring induces some colouring of the ring, and the question is whether it extends inwards. If every ring colouring extends, the configuration is reducible outright. If some do not, one may still try to repair them with a Kempe chain : given a colouring, pick two colours and consider a connected component of the subgraph using only those two: interchanging the two colours throughout that component leaves a proper colouring, but a different one, which may extend where the original did not. A configuration for which every ring colouring either extends or can be brought by such interchanges to one that does is called D-reducible. When that fails, a weaker test called C-reducibility allows the configuration to be modified first — contracting part of it — before the extension test is applied. Every member of an unavoidable set being reducible, the minimal counterexample must contain something it cannot contain, and the theorem follows. The machine's task was to run these tests, and to assist with the unavoidability analysis, which was too large to complete by hand. The objection, in its strongest form The philosophical complaint was put most sharply by Thomas Tymoczko in 1979: the classical demand is that a proof be surveyable, meaning that a competent reader can check each step and hold the whole argument in view, and a proof that must be taken on the word of a machine imports an empirical element into mathematics. The Appel–Haken proof fails surveyability, and the failure is permanent rather than a matter of anyone's patience. The scale is worth making concrete. Consider one configuration whose ring has fourteen vertices. The ring is a cycle, and the number of ways to colour a cycle of $n$ vertices with $k$ col