The Four Color Theorem

In 1852 a young Englishman named Francis Guthrie was coloring a map of the counties of England and noticed something odd: he never seemed to need more than four colors to keep every pair of bordering counties distinct. Was four always enough, for any map you could ever draw?

The rule is tiny. Color the regions of a flat map so that any two regions sharing a border get different colors. (Touching at a single point doesn't count.) Try it on a globe, a subway map, a cartoon of imaginary kingdoms — four colors always seem to suffice.

That innocent observation resisted proof for 124 years. And when the answer finally came in 1976, it arrived in a way that split the mathematical world: the first major theorem whose proof no human could fully check by hand.

Here is a small map. Click a region to cycle it through four colors. Your goal: make sure no two regions that share a border end up the same color. One of the layouts genuinely needs all four — three will never be enough.

<p class="hint">{{hint}}</p>
<svg id="map" viewBox="0 0 300 215" role="img" aria-label="{{map_aria}}"></svg>
<div class="status" id="status">{{status_initial}}</div>
<div class="btns">
  <button id="check" type="button">{{btn_check}}</button>
  <button id="solve" type="button">{{btn_solve}}</button>
  <button id="reset" type="button" class="ghost">{{btn_clear}}</button>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
#map { width: 100%; max-width: 360px; height: auto; display: block; margin: .3rem 0;
       border: 1px solid #cdd9e3; border-radius: 10px; background: #f6f9fb; }
#map path { stroke: #1d3557; stroke-width: 1.8; cursor: pointer; transition: fill .12s; }
#map text { font: 700 14px system-ui, sans-serif; fill: #1d3557; pointer-events: none; }
.status { font-size: 1rem; font-weight: 600; margin: .5rem 0; min-height: 1.4em; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }

// Code not found

Notice the asymmetry. Checking a finished map is effortless: walk over each border and confirm the two sides differ. Finding a valid coloring by hand can take real searching — press Solve it and the computer backtracks through color choices until every border is satisfied. For a handful of regions that's quick; as maps grow, the number of colorings to consider can blow up.

What exactly was proven, and what stays hard?

• It's settled — and four is the magic number. In 1976 Kenneth Appel and Wolfgang Haken at the University of Illinois proved that every planar map can be colored with four colors. Their strategy: show that any map must contain one of an unavoidable set of configurations, and that each one is reducible — a four-coloring of the rest always extends to it.
• A computer checked 1,936 cases. That unavoidable set was huge. Verifying every configuration by hand was hopeless, so they wrote programs that ground through roughly 1,936 cases (later refined to 1,482). It was the first famous theorem whose proof leaned essentially on a computer — and many mathematicians were uneasy about a proof they couldn't read in full.
• Doubt, then confirmation. In 1997 Robertson, Sanders, Seymour and Thomas produced a cleaner computer proof, and in 2005 Georges Gonthier verified the whole thing inside the Coq proof assistant, machine-checked end to end.
• The cousin is brutally hard. Asking whether a map needs only three colors — or coloring an arbitrary, non-planar graph — is NP-complete. Four colors for planar maps is a gift; three colors is a wall.

That is the twist: the headline result is proven and reassuring — four always works — yet it sits one notch away from graph coloring, which is as hard as anything in P vs NP.

"Give every item a label so that things in conflict never share one" is one of the most common shapes a real problem takes, and map coloring is its friendly face:

• Scheduling: exams or meetings that share a participant must land in different time slots — colors are the slots.
• Radio and mobile frequencies: nearby transmitters need different channels to avoid interference, exactly like bordering regions.
• Compilers (register allocation): variables alive at the same moment can't reuse the same CPU register; compilers color a conflict graph to assign them.
• Seating, teams, and conflict resolution: any "keep these two apart" rule is an edge waiting to be colored.

Learn why four colors suffice for maps and you've met graph coloring — the engine under graph coloring, scheduling and a host of real allocation problems.

The Four Color Theorem hides a double surprise. Mathematically, the answer is generous: four colors are always enough for any flat map, no exceptions, finally proven by Appel and Haken in 1976. But the way it was proven broke new ground — a computer marched through nearly two thousand cases that no person could check alone, forcing mathematics to ask what a proof even is.

So the next time you idly color in a map and never reach for a fifth crayon, remember: you are touching a question that took 124 years, a computer, and eventually a fully machine-checked proof to settle — and whose three-color sibling, like graph coloring, remains genuinely hard.