math graph-theory computer-science history combinatorics

The Four Color Theorem: How Computers Proved a Map Puzzle

In 1852, a mathematics student in London named Francis Guthrie was coloring a map of the counties of England. He noticed something curious: no matter how he arranged his colors, four always seemed to be enough to ensure that no two neighboring counties shared the same shade. He mentioned the observation to his brother Frederick, who passed it along to the distinguished mathematician Augustus De Morgan. De Morgan was immediately intrigued — and immediately stumped. On the very same day the question reached him, he wrote to Sir William Rowan Hamilton: "If a figure be anyhow divided and the compartments differently coloured so that figures with any portion of common boundary line are differently coloured — four colours may be wanted, but not more." Hamilton replied three days later, uninterested. He was busy with quaternions.

That offhand note began a 124-year odyssey — one of the longest open problems in mathematics — that ended not with an elegant proof anyone could read in an afternoon, but with a computer churning through over a billion cases across more than 1,200 hours of machine time. When Kenneth Appel and Wolfgang Haken announced their solution in June 1976, mathematicians around the world celebrated, argued, and questioned whether what had been produced was really a proof at all.

The Concept

The Four Color Theorem states: Any map — a division of the plane into any number of contiguous regions — can be colored using no more than four colors such that no two regions sharing a border have the same color.

The rule is strict about what "sharing a border" means: two regions are adjacent only if they share an edge, a full boundary segment. Regions that touch at a single point — the way Colorado and Arizona meet at the Four Corners — don't count as adjacent and can share a color.

To see why four is needed at all, consider four countries, each of which shares a border with all three others. You need a distinct color for each one, so you need at least four. And such a configuration is geometrically possible on a flat map — draw a triangle, put a fourth region in the center touching all three sides. That's four mutually adjacent regions: four colors required.

The deeper question — why four colors are always sufficient, no matter how fantastically complicated a map gets — is what took 124 years to answer.

Modern mathematics restates this in the language of graph theory. Turn each region into a dot (a vertex) and draw a line (an edge) between any two dots whose regions share a border. What you get is a planar graph — a network of nodes and connections that can be drawn on a flat surface without any edges crossing each other. The Four Color Theorem says: the chromatic number (the minimum number of colors needed so no two connected vertices share a color) of any planar graph is at most 4.

Why It Matters

The theorem matters for two completely different reasons.

The first is purely philosophical: it's a statement about the structure of flat surfaces, a deep fact about the geometry of the plane that isn't obvious and wasn't easy to prove. For a century, some of the sharpest mathematical minds in the world couldn't crack it. The difficulty is not in the concept — a child can understand the problem — but in the proof.

The second reason is entirely practical. Graph coloring is one of the most useful abstractions in computer science, and the Four Color Theorem is the most famous result in that family.

Register allocation in compilers. When a compiler translates a program into machine code, it needs to assign variables to the CPU's limited pool of registers. Two variables that are "live" at the same time — both in use simultaneously — cannot share a register. Model variables as vertices and simultaneous-liveness as edges, and you have a graph coloring problem: color the graph with k colors (the number of available registers) such that no two adjacent vertices share a color. The foundational paper establishing this framing was published by Gregory Chaitin at IBM in 1982, and register allocation based on graph coloring is still used in production compilers today.

Frequency assignment in wireless networks. Cell towers that are geographically close enough to interfere with each other cannot broadcast on the same frequency. Model towers as vertices, potential interference as edges: you need to color the graph (assign frequencies) so that adjacent towers differ. The Four Color Theorem doesn't directly solve the problem — wireless networks aren't planar — but the underlying graph coloring framework is identical, and the theorem's techniques inform the algorithms used in spectrum management.

Exam and job scheduling. If two exams share students, they cannot run simultaneously. Map exams to vertices, scheduling conflicts to edges: a proper coloring gives a valid schedule, with each color representing a time slot. The same structure governs factory scheduling, processor instruction scheduling, and classroom allocation.

The abstract math and the practical engineering share the same skeleton.

The Details

A Proof That Stood for Eleven Years — Then Fell

The first person to claim a proof of the Four Color Theorem was Alfred Kempe, a London barrister who had studied mathematics under Arthur Cayley. In 1879, he published his argument in Nature and in the American Journal of Mathematics. The mathematical community accepted it. Kempe was elected a Fellow of the Royal Society, partly on the strength of this work.

Kempe's core insight was elegant: he invented what are now called Kempe chains, sequences of regions where two colors alternate. If a troublesome region had too many neighbors, you could swap colors along one of these chains to free up a color slot. It was a beautiful idea, and it almost worked.

For eleven years, no one noticed the flaw. Then in 1890, a young lecturer named Percy John Heawood found it. Kempe's argument broke down when handling a region with five neighbors. To free up a color for such a region, Kempe needed to run two separate Kempe chains simultaneously — but these two chains could intersect at a shared vertex. Swapping colors along one chain changed the structure of the other, and the recoloring argument collapsed. Heawood provided an explicit example showing the failure and published his correction in a paper called Map Colouring Theorem.

Heawood salvaged something from the wreckage. He proved the weaker Five Color Theorem — that five colors always suffice — using a corrected version of Kempe's approach. The argument is not complicated: Euler's formula for planar graphs guarantees that every such graph has at least one vertex with five or fewer neighbors. Remove that vertex, color the rest of the graph with five colors by induction, then reinsert the removed vertex — since it has at most five neighbors, at least one of the five colors is free. Done.

The hard step — cutting from five to four — is what required a century.

Kempe chains themselves, despite the flawed proof they were invented for, survived and became essential tools for everyone who came after.

The Algorithmic Turn

By the middle of the twentieth century, mathematicians had a clearer picture of why the problem was hard. Any proof would need to identify a finite list of unavoidable "configurations" — local patterns that must appear in any planar map — and then show that each configuration was reducible, meaning any map containing it could be simplified to a smaller map and then recolored.

Heinrich Heesch developed both of these ideas systematically in the 1960s and early 1970s, and he believed a computer could finish the job. He never got the computing resources to complete the program.

Kenneth Appel and Wolfgang Haken at the University of Illinois at Urbana-Champaign began collaborating in 1972, assisted by John Koch on the algorithmic side. They had access to university computing facilities. The strategy they pursued had two interlocking components:

Discharging (proving unavoidability). Imagine assigning "charges" to every vertex and face of a triangulated planar graph, according to how many edges meet there. Euler's formula — V − E + F = 2, where V is vertices, E is edges, and F is faces — guarantees that the total charge is always positive. The charge cannot be uniformly flat. By redistributing charge according to a set of "discharging rules," any planar graph is forced to contain at least one configuration from a specific unavoidable set. No minimal counterexample could avoid all of them.

Reducibility (proving each configuration can be collapsed). Each configuration on the unavoidable list must be shown reducible: a map containing it can be shrunk to a smaller map, recolored with four colors, and then the coloring extended back to the original. This step required checking billions of sub-cases.

Appel and Haken announced the completed proof in June 1976. The University of Illinois mathematics department commemorated it with a postmark on all outgoing mail: "Four Colors Suffice."

The original proof checked 1,936 reducible configurations using more than 1,200 hours of computer time across three different machines. (A later correction by Ulrich Schmidt, incorporated in the 1989 book, revised the count to 1,476 configurations.)

The Controversy

The mathematical community's reaction was not unanimous celebration. The proof was the first proof of a major theorem in which a computer played an essential, non-checkable role, and this set off a genuine philosophical argument about what a proof is.

The objections were serious. No human could verify the computer-checked reducibility cases in a lifetime. The journal referees had checked the discharging procedure by hand but relied on independent computer programs for the reducibility step. Could you trust the hardware? A compiler bug, a memory error, a hardware fault — any of these could silently corrupt a result without anyone knowing. Mathematics had always rested on proofs that a careful reader could follow from axioms to conclusion. The Appel-Haken proof required trusting machines.

There was also an aesthetic objection. The proof demonstrates that the theorem is true without explaining why it is true. It is, in the words of mathematician Ian Stewart, "a kind of monstrous coincidence." A proof is supposed to illuminate the structure of a problem, to reveal why things must be the way they are. A case-by-case exhaustion of 1,936 configurations illuminates nothing. It simply rules out every possible way the theorem could be false.

The Story Continues

In 1997, a team of four — Neil Robertson, Daniel P. Sanders, Paul Seymour, and Robin Thomas — published a substantially cleaner proof. It reduced the unavoidable set to 633 configurations (down from 1,936) and required only 32 discharging rules (down from over 300). Their algorithm ran in quadratic time rather than quartic time, and the entire verification took about 20 minutes on modern hardware rather than 1,200 hours. The source code was made publicly available.

The proof still required a computer, but it was far more transparent.

In 2005, Georges Gonthier took a different approach entirely: he formalized the proof inside Coq, a proof assistant that verifies logical arguments mechanically according to strict rules of formal logic. The Coq kernel itself is the only component that must be trusted — a tiny, well-audited piece of software compared to the sprawling computer programs Appel and Haken had used. The Coq verification largely answered the "can we trust the machine?" objection by making the verification itself a mathematically rigorous object.

Why Four, Specifically?

The answer has two halves.

Why not three? The complete graph K₄ — four vertices each connected to every other three — requires four colors, and K₄ can be embedded in the plane without edge crossings. (Draw a triangle; put a fourth point inside it connected to all three corners.) So three colors provably aren't enough for all planar maps.

Why not five or more? Heawood's five-color proof shows five always suffice. The gap between "five are sufficient" and "four are sufficient" is the entire difficulty of the theorem. Euler's formula does most of the work for five; getting to four requires the 633-case machinery.

Here's a striking contrast: if you move from a flat plane to a torus — the surface of a donut — the answer changes to seven. On a torus, maps can require up to seven colors, and seven always suffice. This was proven in 1968. The flat plane is uniquely special; the four-color bound is a consequence of the specific topological constraints of a flat surface, not a general truth about coloring.

Takeaways

  • The Four Color Theorem states that any map on a flat surface can be colored with four colors so no two neighboring regions share a color — a fact conjectured in 1852 and proven in 1976.
  • The first claimed proof (Kempe, 1879) was wrong, and the error wasn't found for eleven years, illustrating how hard it is to catch subtle flaws even in published, accepted mathematics.
  • The 1976 Appel-Haken proof was the first major theorem proven by computer, requiring 1,200+ hours of machine time and sparking a philosophical debate about what counts as a mathematical proof.
  • Graph coloring — the theorem's abstract setting — is one of the most practically important concepts in computer science, underlying compiler register allocation, wireless frequency assignment, and scheduling problems.
  • A cleaner proof (1997) and a formally verified one (2005) followed, but the Four Color Theorem still has no short, human-readable proof. If one exists, it hasn't been found.
  • The magic number four is specific to flat surfaces. Change the geometry — move to a torus — and the magic number becomes seven.

Resources:

Originally published at travispickens.com

Back to posts