I built a small thing this week: a page that colors a map of the United States so that no two
bordering states share a color, using only four colors, while you watch. It's a toy. But it sits
on top of a theorem with the most interesting backstory in math — one that, fifty years ago, forced
an argument we are now having again about AI.
▶ Play the interactive version (or read the code on GitHub).
Four colors, always
Here's the claim, called the four-color theorem: any map you can draw can be colored with just four
colors so that no two regions sharing a border get the same one. Not most maps. Any map. Try to
invent one that needs five and you will fail, every time, forever.
It's the kind of statement that sounds like it should be easy to prove. It was not. It sat open for
over a century, outlasting a famous wrong proof that stood for eleven years before someone found the
hole. The thing that makes it hard is the "any map" part: you can't check them one at a time,
because there are infinitely many.
What my page actually does
Coloring a map is really a graph problem in a costume. Turn each state into a node, connect any two
states that share a border, and the question becomes: can I label every node with one of four colors
so no two connected ones match? My page draws the real United States — actual state shapes, Alaska
and Hawaii included — and colors it in, so you're watching genuine graph coloring on a map you
recognize.
The method is the most honest one I know: guess, and back up when you're wrong. Go state by state,
give each the first color that doesn't clash with a neighbor you've already colored, and if you get
stuck with nothing legal left, walk back and recolor the previous state. It's called backtracking,
and it's the same move you make doing a hard sudoku — commit, hit a wall, un-commit, try again.
The whole thing fits in a screen of TypeScript:
type Color = 0 | 1 | 2 | 3;
type Graph = Record<string, string[]>; // state -> the states it borders
function fourColor(graph: Graph): Record<string, Color> | null {
// Try the most-connected states first — this one line is the whole ballgame.
const states = Object.keys(graph).sort((a, b) => graph[b].length - graph[a].length);
const color: Record<string, Color> = {};
const fits = (s: string, c: Color) => graph[s].every(n => color[n] !== c);
const place = (i: number): boolean => {
if (i === states.length) return true; // every state colored: done
const s = states[i];
for (let c = 0 as Color; c < 4; c++) {
if (!fits(s, c)) continue; // c clashes with a neighbor
color[s] = c;
if (place(i + 1)) return true; // worked — move on
delete color[s]; // dead end — undo and try the next color
}
return false; // nothing fit here; make the caller back up
};
return place(0) ? color : null;
}
That's it — twenty lines, no library. The fits check enforces the rule, the loop tries four
colors, and the delete is the backtrack: when a state has no legal color, we erase it and let the
previous state try something else.
Watch it run and two things are satisfying. Four colors really is always enough. And no border ever
ends up joining two matching states — the theorem holding, in front of you, instead of on a page.
The thing I didn't expect
Here's the part that turned a weekend toy into something I actually learned from.
The order you color the states in doesn't change the answer. It changes the work by a factor I had
to recount to believe. Color the most-connected states first — the ones hemmed in by the most
neighbors, where mistakes are cheapest to catch early — and the whole US falls in 115 steps with
zero backtracking. Color them in alphabetical order instead and the same algorithm, looking for the
same four colors, grinds through sixteen million steps and four million backtracks to reach the
identical map.
Same problem. Same code. One decision — which state to try first — and a hundred-and-fifty-thousand-fold
difference in effort. That's the whole reason "just pick a smarter order" is one of the highest-leverage
things you can do to a search like this, and it's invisible until you measure it. The page lets you flip
between the two and watch the backtrack counter either sit at zero or spin like a taxi meter.
Why this theorem, out of all of them
Now the backstory, which is the real reason I wanted to write this.
The four-color theorem was finally proved in 1976. And it was the first major theorem in history
whose proof required a computer — not as a convenience, but because no human could do it by hand.
The proof worked by grinding down "any map" to a large but finite pile of specific configurations,
roughly nineteen hundred of them, and then having a machine check every single one. No person has
ever verified that proof end to end by reading it. No person ever will. There's too much, and the
only thing that can hold all of it is a computer.
That broke something open, and the fight was bitter. A proof had always meant something a human mind
could follow, step by step, and be convinced. This one asked mathematicians to accept a true
statement on the word of a machine they couldn't audit. Some refused. Some still call it
unsatisfying — correct, they'll grant you, but not illuminating, because you finish it without the
feeling of understanding why it's true. You just know that it is, because the computer said so and
the computer was careful.
Sit with that for a second, because we are having the exact same argument right now, fifty years
later, about something that feels brand new.
The oldest version of a question we think is new
When I use an AI to help me build something, the useful part isn't that it types fast. It's that it
will check more cases than I will, more patiently than I will, and surface the one I'd have skipped.
And the uncomfortable part is the same shape as 1976: at some point I'm accepting an output I did not
derive myself and could not fully re-derive in reasonable time. I trust it because the process that
produced it is sound, not because I personally walked every step.
The four-color theorem is the fifty-year-old version of that trade, made clean. It asks the question
without any of the hype or fear attached to the word "AI": do you accept a conclusion you can't
reason all the way through yourself, if the method that produced it is trustworthy? Mathematicians
have had to live with "yes, carefully" since 1976 and the sky didn't fall. The theorem is true. The
discomfort it caused was real, and it was also survivable, and both of those are worth remembering
the next time someone tells you a machine-checked result either can't be trusted or must be.
The honest answer, then and now, isn't trust or distrust. It's: know exactly which part the machine
did, make sure that part is the kind of thing a machine does well — exhaustive, checkable, boring —
and keep the judgment about what to even ask for firmly on your side of the line. That's not a
compromise with the tool. That's the whole skill.
The interactive map and a headless version of the solver are in my code-samples repo — run the terminal version and watch the ordering difference yourself, or flip the interactive page between "smart" and "shuffle" and see the backtracks pile up.
Top comments (0)