In 1852, a young South African student named Francis Guthrie was coloring a map of the counties of England when he noticed he never seemed to need a fifth color. Four were always enough to ensure that no two neighboring counties matched. He wondered whether four would suffice for any map — and mentioned it to his brother, who mentioned it to his professor, the logician Augustus De Morgan, who was so taken with the question that he began writing letters about it the same day.
It looked like homework. Any child with crayons can test it; any patient adult feels its truth after an afternoon. Surely a proof was a week away.
It took 124 years, destroyed at least one celebrated career achievement, and ended in a form so alien that philosophers still argue about it: the first major theorem in history proved with the essential help of a computer — a proof no human being has ever read in full, or ever will.
A decade of false certainty
The four color problem quickly revealed its trap: the gap between verifying instances and proving all cases. Every map anyone colored obeyed the rule, but "every map" is an infinite space, and infinity does not care about your examples.
In 1879, the British mathematician Alfred Kempe published a proof. It was elegant, it was celebrated, and Kempe was elected a Fellow of the Royal Society with the result glowing on his record. For eleven years the four color theorem was, as far as the mathematical world knew, settled.
Then, in 1890, Percy Heawood found the flaw — a subtle failure in how Kempe's argument handled one configuration. The theorem reopened, and the episode entered mathematical folklore as a permanent caution: a proof believed by everyone can still be wrong, and eleven years of nobody noticing is not evidence. Heawood salvaged what he could, showing Kempe's machinery does prove that five colors always suffice. Four remained out of reach for another 86 years. There is a lesson for solvers buried in the wreckage: Kempe's central tool — chains of alternating colors, flipped to free up a color elsewhere — survived him. It remains a standard weapon, and advanced Sudoku players use its direct descendant every time they flip a chain of paired candidates to break a deadlock.
The unreadable proof
The proof that finally landed, in 1976, came from Kenneth Appel and Wolfgang Haken at the University of Illinois, and it worked by an audacious division of labor.
The human part: show that every conceivable map must contain at least one configuration from a specific finite catalog — and that each catalog entry is "reducible," meaning any map containing it can be shrunk to a smaller map such that a four-coloring of the smaller one extends back to the original. If every entry is reducible, no smallest counterexample can exist, and the theorem follows.
The inhuman part: the catalog held 1,936 configurations, and checking reducibility for each required case analysis far beyond any lifetime of pencil work. Appel and Haken gave that half to the computer — around 1,200 hours of 1970s machine time, grinding through billions of cases no person would ever see. The University of Illinois mathematics department celebrated by changing its postage meter to read FOUR COLORS SUFFICE.
Not everyone celebrated. A proof, tradition held, is something a mind can survey — follow from beginning to end and see the necessity of. This one nobody could survey. The philosopher Thomas Tymoczko argued in 1979 that mathematics had quietly become, in part, an empirical science: we believe the four color theorem the way we believe a telescope, by trusting an instrument. Mathematicians largely made their peace — especially after 1997, when a team including Neil Robertson and Robin Thomas rebuilt the proof with a leaner catalog of 633 configurations, and 2005, when Georges Gonthier went one better and had the entire argument, logic and computation alike, verified line-by-line by a proof assistant whose tiny kernel is itself checkable by hand. The response to "we can't read the computer's work" turned out to be a second computer that reads it perfectly, every time.
What this has to do with your morning grid
More than you might think. Graph coloring — assigning labels to regions so that neighbors differ — is not just like a logic puzzle; it is the formal skeleton of several you already play. Sudoku is graph coloring with nine colors, as we explored in our essay on the mathematics of the grid. Every puzzle that forbids matching neighbors, from map-style region games to link-routing grids, lives in Guthrie's world.
But the deeper connection is the trust model. When you sit down to one of our puzzles, you are extending exactly the trust that made philosophers nervous in 1976: a machine has checked, case by exhaustive case, something no human will ever re-derive — that this grid has one solution, reachable by logic, with no dead ends that aren't your own. We have written about how we verify uniqueness before publishing; the four color saga is the intellectual history of why that kind of verification deserves belief. Kempe is the cautionary tale (consensus isn't proof); Appel–Haken is the promise (exhaustive machine checking works); Gonthier is the modern standard (verify the verifier).
The crayon test
The theorem's statement never stopped being child-simple, and that is the best thing about it. Four colors suffice for any flat map — for the counties of England, for a doodle of a thousand squiggly regions, for maps no one has drawn yet. (Mind the fine print: regions must be connected — real-world exclaves can force a fifth color — and meeting at a single point doesn't count as neighboring.)
A question a student can ask while coloring, an answer that required redefining what "proof" means: puzzles run on precisely this voltage difference. The rules fit in a sentence; the truth underneath runs as deep as anyone cares to dig. Somewhere between the crayons and the proof assistant, there is room for a lifetime of Sunday mornings.
