Take any map you like — countries, counties, the wobbliest gerrymander ever drawn — and four colours will always be enough to shade it so that no two regions sharing a border get the same colour. Not usually. Always.
The claim is simple enough for a child to check on a placemat, and it took 124 years to prove: Francis Guthrie noticed it in 1852 while colouring a map of England's counties, and Kenneth Appel and Wolfgang Haken closed it in 1976 [1]. What they handed in was not a proof anyone could read. It was a proof a computer could run — and that started an argument that is, quietly, still going.
Two rules, both load-bearing. A region must be one connected piece; and two regions border each other only if they share a boundary with actual length — touching at a single point does not count. Without that second rule the theorem is trivially false: slice a disc into a hundred pie wedges and all hundred meet at the centre.
Underneath, this is a graph problem, of the kind Euler invented at Königsberg. Put a dot in each region and join two dots whenever their regions share a border; colouring the map is now colouring the dots so that no edge joins two of the same colour. Because the regions lie flat and the borders do not cross, the graph is planar — drawable with no edges crossing.
Three colours fail, four are hard
Four is not an arbitrary number: three genuinely fails, and one small map proves it. Draw a disc, put a small circular region at its centre, and cut the surrounding ring into three sectors. Each outer sector borders the centre, and each borders both of the others along a radial line. So all four regions border all three others, every one needs a different colour, and three is dead.
Next thought: could we find five mutually bordering regions? You will fail, and a theorem says you always will — five mutually connected dots (the graph ) cannot be drawn in the plane without edges crossing.
It is tempting to declare victory there. Do not. "You can't find five mutual neighbours, therefore four colours suffice" is invalid, and spotting why is the whole difficulty.
Here is a counterexample to the reasoning. Draw five regions in a ring, each bordering only its two neighbours. It contains no three mutually bordering regions at all. Yet two colours fail: go around alternating and after five steps you return to a clash, so it needs three. A map can demand more colours than its largest mutually-bordering clump suggests. Colour constraints travel; they are not local.
That gap is where 124 years went. Alfred Kempe published a proof in 1879 and was believed for eleven years, until Percy Heawood found the hole in 1890 — salvaging from the wreckage a proof that five colours always suffice [3]. Between five and four sat another century.
The proof nobody can read
Appel and Haken kept Kempe's shape. Suppose the theorem is false; then among all maps needing five colours there is a smallest. Show that every map contains at least one of a fixed list of local patterns (an unavoidable set), and that each pattern is reducible — a map containing it could be shrunk to a strictly smaller five-colour-needing map. A smallest counterexample containing a smaller one is a contradiction.
The catch is the list. Their unavoidable set held 1,936 configurations, and each one's reducibility was checked by brute force: roughly 1,200 hours of 1976 computer time. No human has ever verified that check by hand, and no human ever will.
Mathematicians did not take it well. A proof had always been something you could in principle hold in your head; this one you could only trust — the code, the compiler, the hardware. Was it a proof, or very good evidence? The philosopher Thomas Tymoczko argued it changed the meaning of the word; others simply waited for it to break, as Kempe's had.
It did not break. In 2005 Georges Gonthier formalised the whole proof in the proof assistant Coq [2], so every step, including the machine checking, is verified by a small, independently trustworthy logical kernel. You still cannot read the proof — but you no longer have to trust anyone's programming to believe it.
What counts as a proof now
Four colours always suffice, and after 2005 that is true in a way even the sceptics accepted. What changed permanently was the job description: computers may now do parts of a proof no human can audit, provided something small and checkable audits the computer.
Two honest caveats. The theorem lives on a flat plane (or a sphere); move to a doughnut and it fails outright — maps on a torus can need seven colours. And real atlases break the rules rather than the theorem. Michigan is not one connected piece: its Upper Peninsula is separated from the Lower by water, and insisting both halves share a colour violates the "one connected region" assumption. Exclaves do this constantly. The theorem is about maps as mathematicians define them — which is exactly the abstraction Euler pulled at Königsberg: keep the connections, throw away the geography.
References:
[1] Kenneth Appel and Wolfgang Haken, "Every planar map is four colorable," Bulletin of the American Mathematical Society 82(5) (1976).
[2] Georges Gonthier, "Formal Proof — The Four-Color Theorem," Notices of the American Mathematical Society 55(11) (2008).
[3] Robin Wilson, Four Colours Suffice: How the Map Problem Was Solved (Princeton University Press, 2002).
Note: "Four colours suffice" assumes every region is a single connected area and that regions meeting at a single point are not treated as neighbours. Real political maps with exclaves — and any map drawn on a surface other than the plane or sphere — sit outside the theorem's hypotheses.