Four colours, and a proof nobody can read
Colour a map so that countries sharing a border get different colours. How many colours are needed, in the worst case, for any map that could ever be drawn on a flat sheet?
The answer is four. It was conjectured in 1852 by Francis Guthrie, who noticed while colouring the counties of England that four always seemed to suffice, and it was not proved until 1976 — after which many mathematicians were not sure they believed it, for reasons that had nothing to do with whether it was true.
Delete the map
The first move is Euler’s, and it is the same move.
Nothing about the colouring depends on the shape of a country, its area, the length of its borders, or where it sits. The only thing that matters is which countries touch which. So throw the geography away and keep a dot for each region and a line between dots whose regions share a border.
That leaves a graph, and the question becomes: colour the dots so that no edge joins two of the same colour. The smallest number of colours that works is called the chromatic number.
One thing survives the deletion and is easy to miss: the graphs that arise this way are special. A map drawn on a plane produces a graph that can be drawn on a plane with no edges crossing — a planar graph — because the regions themselves were laid out without overlapping. The four colour theorem is a statement about planar graphs, and it is false without that word. Take five dots and join every pair: the chromatic number is five, and no map produces it, because that graph cannot be drawn flat without crossings.
Why the wheel needs four
The figure’s map is the smallest honest demonstration that three colours are not enough, and it is worth walking through.
A hub touches five rim regions. The rim regions form a ring, each touching its two neighbours.
Colour the hub first — say red. Every rim region touches the hub, so none of them can be red; the five rim regions must be coloured from the remaining palette. Around the ring, adjacent regions must differ, so what is needed is a proper colouring of a five-cycle.
A cycle of even length can be coloured with two colours, alternating all the way round. A cycle of odd length cannot: alternating around an odd ring brings the first colour back to meet itself at the join. So an odd ring needs three colours, and with the hub that is four.
The generator does not take this on trust. It searches exhaustively for a colouring with one colour, then two, then three, and reports the first count that succeeds — so the number in the caption is the chromatic number rather than an upper bound that happened to be found. It then checks the colouring edge by edge, and it requires the odd-ring case to come out at four and the even-ring case at three.
The alternation is worth recognising, because it is the same parity obstruction that decides whether a walk across Königsberg exists and which regular polygons admit a curve of constant width. In all three the question is whether going once around a cycle returns something to itself or to its opposite, and in all three the answer is decided by one bit — whether a count is odd or even.
That is also why the difficulty does not grow with the number of regions. A ring of seven is exactly as hard as a ring of five, and a ring of a thousand and one is no harder than either. Size is not what makes a colouring problem difficult, which is the first clue that the four colour theorem’s difficulty lies somewhere other than where it appears to.
Five is easy
Before the difficulty, the part that is not difficult: five colours always suffice, and the proof is a page long and entirely readable. It was found by Heawood in 1890.
It rests on a counting fact from Euler’s formula: every planar graph has a vertex of degree at most five. That follows from together with the observation that each face of a planar graph is bounded by at least three edges — the arithmetic forces , so the average degree is under six and some vertex is at most five.
Now argue by induction. Take a planar graph, find a vertex of degree at most five, delete it, colour what remains with five colours by induction, and put back. If its neighbours use at most four colours, a colour is free. The only difficulty is a degree-five vertex whose five neighbours use all five colours — and Heawood’s argument shows the colours can be shuffled along a chain to free one up.
That is the whole proof. It is short, it is checkable, and it gets five.
Getting from five to four took another eighty-six years, and nothing about the five-colour proof suggests where the extra difficulty comes from — which is a recurring and slightly maddening feature of this subject.
The proof that cannot be read
Appel and Haken’s 1976 proof follows a strategy that had been developing since Kempe’s flawed 1879 attempt, and it works in two parts.
Unavoidability. Produce a set of local configurations such that every planar graph must contain at least one of them. This is a finite check on the arithmetic of Euler’s formula, carried out by an accounting technique called discharging.
Reducibility. Show that each configuration in the set cannot appear in a minimal counterexample — because if it did, the graph could be shrunk, coloured by induction, and the colouring extended back.
Together they close the argument: any counterexample must contain a configuration, every configuration is impossible in a counterexample, so there is no counterexample.
The trouble is the size. Their unavoidable set had 1,936 configurations, and checking each for reducibility required a computation that took about 1,200 hours of machine time. No human has verified the case analysis by hand, and no human is going to.
That produced a genuine and lasting argument about what a proof is for. A proof is supposed to explain, and to be checkable by a reader willing to do the work. This one is checkable only by trusting a program, a compiler, and the machine underneath — and in 1976 that was an uncomfortable amount of trust, particularly since the first version contained errors that were found and repaired later.
The response has been to make the trust smaller rather than to remove it. Robertson, Sanders, Seymour and Thomas produced a cleaner version in 1997 with 633 configurations. In 2005 Gonthier produced a proof formally verified in the Coq proof assistant, from the axioms up — so what must now be trusted is the correctness of a proof checker, which is a far smaller and much more scrutinised object than a bespoke program.
That is probably the honest resolution. The proof is not readable and it is verified more rigorously than most readable proofs are, because a machine checking every step does not skip the routine cases the way a human referee does.
It is worth setting this beside the other kind of unproved statement this collection has met. The diagonals in Ulam’s spiral are a visible pattern with no proof at all — Hardy and Littlewood’s prediction matches observation and remains a conjecture. The four colour theorem is the opposite: a pattern with a proof nobody can read. Both leave a reader unable to check the claim personally, and the reasons are entirely different, which is worth keeping separate. One is a gap in mathematics; the other is a gap between mathematics and a human lifetime.
What the theorem does not say
Three misreadings are common enough to be worth heading off, and each marks a real boundary of the result.
It is not about how many colours a given map needs. Most maps need three, many need two, and the theorem only says none needs five. Handed a particular map, it supplies no colouring and no count — it is a statement about the worst case over all maps, which is a different object from any map.
It requires countries to be connected. A country in two disconnected pieces, both of which must take the same colour, breaks it immediately. Real political maps have such countries, so the theorem is not quite a statement about atlases; with disconnected regions allowed, no finite number of colours suffices.
It requires borders to be more than points. Two regions meeting at a single corner are not counted as neighbours — otherwise the wheel maps would already need as many colours as they have spokes, since every rim region touches every other at the centre if points count.
That last figure is the honest lower bound, and it is worth separating from the odd-ring argument. Four mutually adjacent regions obviously need four colours; the interesting question was never whether four are sometimes necessary but whether they are always sufficient, and the picture that settles the first says nothing about the second.
What makes four hard and three easy
There is one more asymmetry worth naming, because it explains why the theorem has the shape it does.
Deciding whether a given graph can be coloured with two colours is easy: two-colourable means no odd cycle, and that can be checked in linear time by walking the graph and alternating.
Deciding whether a given graph needs only three is NP-complete — as hard as any problem in that class, with no known efficient method, and it stays hard even for planar graphs.
Deciding whether four suffice for a planar graph is trivial, because the answer is always yes.
So the difficulty is not monotone in the number of colours. Three is the hard question and four is the easy one, and four is easy only because of a theorem that took a century. Without the theorem, four would be as hard as three. The four colour theorem’s value is that it converts a hard computational question into a constant.
What the picture cannot show
Every figure here is one map. The theorem is about all of them — every map that could be drawn, of any complexity — and no gallery of examples establishes anything about that.
The gap is unusually wide in this case, and history proves it. Kempe published a proof in 1879, it was accepted for eleven years, and Heawood found the flaw in 1890. The flaw was in a case analysis, not in anything a picture would show, and eleven years of mathematicians looking at maps did not turn it up. Tait published another flawed proof in 1880 and it survived eleven years too. If drawing maps were evidence, those would have been caught immediately.
The pictures also cannot show why four. Nothing in the wheel maps suggests that four is where it stops rather than five or six — those figures establish a lower bound, that three is not enough, and lower bounds are the half that pictures can do. The upper bound, that four always suffices, is the entire content of the theorem and has no diagram, in the way a budget argument can rule out a sixth regular solid while constructing the five is separate work.
The same trap as the diagonals in a spiral of primes is present in a different form. There, a visible pattern lacks an explanation. Here, an invisible pattern had an explanation that was wrong for eleven years. In both cases the pictures were consistent with the truth and with the falsehood, and looked identical either way.
The ladder from here
Rungs above: the five-colour theorem proved in full, with Kempe chains drawn. Kempe’s flaw, and exactly which case it missed. Discharging, made concrete on a small unavoidable set. The chromatic polynomial, which counts colourings rather than merely deciding whether one exists. Brooks’ theorem, bounding the chromatic number by the maximum degree. Colouring on other surfaces, where the answer for a torus is seven and — surprisingly — is easier to prove than the plane’s four. Edge colouring and Vizing’s theorem. The NP-completeness of three-colouring. And Euler’s formula, which is doing the counting underneath all of it.
Seven on a doughnut, four on a plane
The last of those deserves a closing paragraph, because it is the most surprising thing in the subject.
Maps on a torus need seven colours, and that was settled by Heawood in 1890 — eighty-six years before the plane’s four. The same is true of every other surface: the formula for the number of colours needed on a surface with handles was known and proved long before the plane’s case, which is the simplest surface of all.
The reason is that the general formula has slack in it. On a complicated surface there is enough room in the counting for a clean argument to close, with a comfortable margin. On the plane the margin is zero — the bound the easy argument gives is five, the truth is four, and there is nothing left over to spend.
That is a pattern worth expecting rather than being surprised by. The easiest instance of a family is frequently the hardest to prove, because it is the one where the general argument’s slack has run out. It is why was the last case of Fermat’s Last Theorem to feel easy and the first to be proved, why small cases of many conjectures are checked by exhaustion rather than by the argument that handles the rest, and why simplest and easiest are different words.