The idea in plain English: On any flat map where regions share borders (not just meeting at a point), you never need more than 4 colors to make sure no two neighboring regions have the same color. Think of a map of U.S. states — even with 50 states touching each other in complex ways, 4 colors is always enough. The puzzle gives you a small planar graph — regions as nodes, borders as edges — and you assign colors 1, 2, 3, 4 so that connected nodes never match.
Why this really exists: The problem was first posed by Francis Guthrie in 1852 when he noticed that coloring the counties of England required only 4 colors. It became one of the most famous unsolved problems in mathematics for over a century. In 1976, Kenneth Appel and Wolfgang Haken at the University of Illinois finally proved it — but their proof required a computer to check 1,936 configurations in over 1,200 hours of Cray supercomputer time. It was the first major theorem in history proved with computer assistance, and it sparked a fierce debate about what counts as a valid proof. Today it's a cornerstone of graph theory.
Consider a simple map with four regions where every region touches every other region:
This is why the theorem says "at most 4" — some maps genuinely need all 4. The puzzle gives you a planar graph (never containing K₅ or K₃,₃ as subgraphs, by Kuratowski's theorem) and asks you to produce a valid coloring.
1. The puzzle gives you a planar graph with N nodes and edges between adjacent regions
2. Nodes represent regions, edges represent shared borders
3. Assign each node a color from {1, 2, 3, 4}
4. No two nodes connected by an edge may share the same color
5. Use a greedy algorithm: order nodes, assign the smallest available color not used by any already-colored neighbor
6. For most planar graphs, a simple greedy approach works — but some graphs need re-ordering to succeed with ≤4 colors
💡 If greedy fails, reorder nodes by descending degree (most neighbors first). The theorem guarantees a 4-coloring exists — you just need to find it.
| Difficulty | What to Expect | Nodes | Approach |
|---|---|---|---|
| 1 | Tiny graph (≤5 nodes), greedy works easily | 4–5 | Any ordering works |
| 2 | Small planar graph, some tricky adjacencies | 6–8 | Greedy with degree sorting |
| 3 | Moderate planar graph, may need backtracking | 9–12 | DSATUR or recursive backtracking |
| 4 | Larger planar graph, constrained coloring | 13–16 | Backtracking with constraint propagation |
⚠️ All graphs are planar — they never require 5 colors. The theorem guarantees a valid 4-coloring exists for every puzzle generated.
Appel and Haken's 1976 proof worked by reducing every possible planar map to one of 1,936 unavoidable configurations, then showing each one was "reducible" (could be 4-colored). Humans could never check this by hand — it took a Cray supercomputer 1,200 hours. This sparked intense debate in the mathematical community:
In 2005, Georges Gonthier and others produced a formalized proof using the Coq proof assistant — a computer-checked logical derivation that removed all doubt. Today, computer-assisted proofs are widely accepted, but the four color theorem remains the landmark case in the debate.