The Proof That Held for Eleven Years

The step, on nine countries

Each disc is a country and each line is a shared border, which is all a map is once you stop drawing coastlines. This one has 9 countries and 21 borders, and it is flat: the drawing below uses straight lines and no two of them cross, which the page checks by testing all 132 pairs of borders that do not already share a country. Eight countries are coloured. Country 0, in the middle, is not, and its five neighbours are wearing all four colours.

The map is drawn. Six steps follow, and every colour on it is recomputed as you move through them.

What Kempe does, in his own order

The five neighbours carry four colours, so one colour is on two of them, and those two are never next to each other around the ring. Exactly one neighbour sits between them. Kempe calls that one v1 and reads the ring from there: v1 v2 v3 v4 v5, with the doubled colour on v2 and v5. On this map that is colours A C D B C.

A chain is what he invented for this and what carries his name. Pick two colours; the countries wearing them break into connected islands; swap the two colours throughout any one island and the map is still properly coloured, because nothing outside the island wears either colour next to it. That is the whole idea, and it is correct.

Two chains would end the case on their own:

If either chain missed its target, swapping it would take colour A off v1 and leave A free for country 0. On this map both reach, so both escapes are shut, and Kempe is down to his last move.

That move is two chains at once. The C/B chain at v2 cannot reach v4, because the A/D chain from v1 to v3 plus country 0 closes a loop with v2 inside it and v4 outside, and no C or B country can cross a fence made of A and D countries. By the same argument the C/D chain at v5 cannot reach v3. Swap the first and v2 stops being C. Swap the second and v5 stops being C. Then C is free and country 0 takes it. Every sentence of that is true.

Both chains are safe. Therefore both may be swapped.

That is the sentence, and it does not follow. Each chain was proved safe in the colouring as it stands. Swapping one of them changes the colouring, and the proof that the other was safe was a proof about a map that no longer exists.

That is not a modern reading of it either. The notice of Heawood's paper in the Jahrbuch über die Fortschritte der Mathematik for 1890 puts the flaw in one sentence, and it is this one: the simultaneous execution of two colour interchanges, each of which is admissible on its own, need not always be possible. Everything below is that sentence, made operable.

There are only two ways to read the instruction, and this map breaks both. Read as written, both islands are the ones you found before you touched anything, and you recolour both. Countries 4 and 7 then both end up C, and they share a border: 1 broken border out of 21. Read as one and then the other, the colouring survives, but the second island is no longer the island that was proved safe. It has grown to 4 countries, it now reaches v3, and swapping it puts C straight back on the ring. The five neighbours still wear four colours. Nothing is freed.

Then just do more swaps

The obvious objection, and it deserves a number rather than a paragraph. From this colouring there are 24 single chain swaps available (8 coloured countries, 3 other colours each), collapsing to 9 distinct results. The page runs all of them. The number that free a colour for country 0 is 0. Kempe's move is not merely mis-argued here; on this map no single swap of any kind gets country 0 coloured.

Two swaps do. Searching outward from the stuck colouring, the page finds 8 colourings at depth two that free a colour, which are the earliest escapes any argument of this kind could reach. Keep going and the search closes: 192 colourings are reachable in all, of which 48 free a colour. Counted separately and from scratch, the map minus country 0 has exactly 192 proper four-colourings, so the chain swaps reach every one of them. Nothing is stranded.

And the map itself is fine. Enumerated exhaustively, it has 48 proper four-colourings, and the first one the enumeration finds is printed under the table above, with all nine countries coloured. Note that the colouring the instrument works on is not one of those 48: its ring wears all four colours, which is exactly why country 0 is stuck. What broke was not the theorem and not this map. It was the argument, and an argument has to work on every map at once.

Is this a freak map?

A single counterexample invites the reply that it was hunted for. So count them all. The page generates every triangulated map on a given number of countries, by walking the diagonal-flip graph, which Wagner proved in 1936 is connected for a fixed vertex count. The counts are not asserted: they are checked against the published enumeration of simplicial polyhedra, 1, 1, 2, 5, 14, 50, 233, 1249, 7595 for 4 to 12 nodes (OEIS A000109). Then Kempe's fifth case is run over every four-colouring of every one of them, one representative per renaming of the colours.

Below 9 countries the step never breaks. At 9 it does, on 2 of the 50 maps that exist. Across all 9150 maps up to 12 countries, 533 contain a colouring the step gets wrong. The table runs itself out to 10 countries; the buttons under it take it to 12, which is where those two totals come from, and it prints its own count against A000109 at every size on the way.

The two readings do not fail in the same places. Read as written, the step breaks on 2131 of the 31910 colourings that reach it. Read one after the other, it fails on 1012, and measured over all 9150 maps every one of those 1012 is also in the 2131. The chains actually overlap in only 866 cases, so sharing a country is not the mechanism. The mechanism is simply that the first swap moves the ground the second one was standing on.

Yes, and then computers did it. Everyone knows that

This is the sophisticated reader's move and it is worth stating at full strength rather than in a footnote:

Kempe was wrong, fine. But the theorem is true and Appel and Haken settled it in 1976 by running Kempe's argument on a machine, over more cases than a person could check. So the interesting content is that the proof got big, not that Kempe got it wrong. Give it enough compute and the fifth case goes through.

The first half of that is right and the page will not pretend otherwise. Appel and Haken's proof is a proof. It was independently reproved twenty years later, and the reproof was then machine-checked. The second half is the part that is wrong, and the thing that shows it is finite, small enough to run here, and gives different answers to different configurations.

What replaced Kempe's move is not more Kempe. It is reducibility, and it asks a different question. Stop asking about maps. Take a fixed patch of countries with a ring of countries around it. Cut the patch out of any map at all, four-colour whatever is left, and the ring comes back wearing some colouring. Now ask: from every colouring the ring could possibly wear, and whatever the vast unknown outside turns out to look like, can chain swaps out there always reach a ring colouring the patch itself can absorb? If yes, the patch cannot appear in a smallest bad map, and the patch is reducible. That question is finite. It does not mention maps, or sizes, or induction. It is a property of the patch alone, and a browser can answer it.

Two flavours, and the difference matters. D-reducible means the chain swaps alone finish the job, exactly as described above. C-reducible means they do not, and the argument only closes if you are also allowed to modify the configuration itself, contracting or deleting inside it, before appealing to minimality. Appel and Haken needed both, and so did the 1997 rebuild: in its published set of 633 configurations, 249 are settled by D-reducibility alone and the other 384 need a contraction too. So D is not most of the modern proof. It is the smaller and more honest part of it. Everything on this page is D, because it is the part a reader can watch run to the end.

The rules the outside is allowed to obey

The whole content of planarity sits in two facts about what the deleted outside can do to the ring, and both are load-bearing.

One. Two ring countries that are next to each other and both wear a colour of the pair being swapped are in the same island, by force. Two. Chains on two colour pairs with no colour in common cannot cross, because they are drawn in a plane and share no country. So the way the outside joins up ring positions into islands is a non-crossing partition, and the two halves of a colour split are non-crossing against each other. The checker below sweeps over every non-crossing possibility and takes the worst one for the reader every time: it clears a ring colouring only if an escape exists under every arrangement the outside could have, and leaves it standing if even one arrangement traps it.

Run the ring of five, the case Kempe could not finish. Its ring can wear 240 colourings, of which 120 the single country inside can absorb, because it only needs one colour left over. The other 120 are the hard ones, and the sweep removes none of them. Not some. Not most after a long run. Zero, on the first pass, and the fixed point is reached immediately. There is no amount of compute that changes this, because it is not a search that gave up. It is a complete answer, and the answer is no.

Now run Birkhoff's diamond, four countries inside a ring of six, the first configuration of ring size six shown to be reducible, and the first with more than one country inside (Birkhoff, 1913). The three- and four-neighbour cases above it are older; they are Kempe's, and the panel credits them to him. Same machinery, same code path. Its ring wears 732 colourings, the patch absorbs 384 of them, and 348 are hard. The sweep clears them in five passes, and this is the staircase: 348, 252, 192, 96, 24, 0. That staircase is the finite check Kempe did not have, running to its end.

Those 384 absorbed colourings are the same colouring 16 times over once you stop caring which colour is called which: they fall into 16 classes under the 24 renamings. That number can be looked up rather than taken on trust. Robertson, Sanders, Seymour and Thomas published the data behind their 1997 proof, and the diamond is the first of their 633 configurations, filed as 0.7322 with the header 10 6 16 0: ten countries, ring size six, and a, the number of ring colouring classes the patch absorbs, equal to 16. Nothing on this page was tuned to that number and nothing here reads their file. The check below recomputes it.

And the ring of six with a single country inside is the control that makes the point sharp. It has the same ring size as the diamond, the same 732 colourings, and goes through the same code. Its verdict is the opposite: 480 hard colourings, 480 still standing at the end. The instrument is not a compute meter. It is a discriminator, and what it discriminates on is the patch, not the effort.

That is the answer to the dismissal. Under the reading that computers just ran Kempe harder, these three configurations differ only in how long they take. Under the reading that something else replaced Kempe, they differ in kind, and two of them are settled negatively for ever. The page produces the second output, not the first.

What the machine actually did, and what it cost

The 1976 proof has two halves and reducibility is only one of them. The other is unavoidability: proving by a discharging argument that every map must contain at least one patch from a fixed list. Kenneth Appel and Wolfgang Haken published the discharging half, and with John Koch the reducibility half, as two papers in the same volume of the Illinois Journal of Mathematics in 1977. The list ran to well over a thousand configurations and the reducibility checks took more than a thousand hours of machine time. Robertson, Sanders, Seymour and Thomas rebuilt the whole thing in 1997 with 633 configurations and a quadratic-time colouring algorithm, and in 2005 Georges Gonthier and Benjamin Werner formalised it inside Coq.

That last step is the one worth naming. Before it, believing the theorem meant believing a pile of purpose-written programs nobody had verified, and the honest position was that no human had read the proof end to end. After it, the trust moved into a proof kernel: a small, general, heavily examined checker that had no idea it was doing graph theory. The proof did not get shorter. It got checkable by something other than stamina.