difficulty levels — click green to claim

> FOUR COLOR THEOREM

four-color difficulty: 1–4 also known as: four color map theorem, four color problem

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.

▸ Concrete Example: A 4-Region Map

Consider a simple map with four regions where every region touches every other region:

Regions: A, B, C, D
Borders: A-B, A-C, A-D, B-C, B-D, C-D (a complete graph K₄)

Can we color this with 3 colors? Let's try:
A → color 1
B → color 2 (different from A)
C → color 3 (different from A and B)
D → ??? (must differ from A, B, AND C — all 3 colors are used!)

D must be color 4 — 3 colors are not enough for K₄

One valid 4-coloring:
A = 🔴 Red (1), B = 🟢 Green (2), C = 🔵 Blue (3), D = 🟡 Yellow (4)

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.

▸ How to Color a Planar Graph (Step by Step)

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

# Python greedy graph coloring (may need node reordering):
def four_color(graph):
    # graph: adjacency dict {node: [neighbors]}
    colors = {}
    for node in graph:
        used = {colors[n] for n in graph[node] if n in colors}
        for c in range(1, 5):
            if c not in used:
                colors[node] = c
                break
    return colors

# For harder cases, try ordering by degree (largest first):
# sorted(graph, key=lambda n: len(graph[n]), reverse=True)

💡 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 & Puzzle Patterns

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.

▸ The Controversy: When a Computer Proves a Theorem

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:

Can a proof be valid if no human can verify it? Traditional proofs must be checked line by line by a mathematician.
What if the computer had a bug? The proof was tied to specific software and hardware that could have errors.
Is it mathematics or engineering? Critics called it a "brute-force enumeration" rather than an elegant proof.

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.

▸ Real-World Connections

Scheduling: Assigning time slots to classes or exams so no student has a conflict — rooms/subjects are nodes, conflicts are edges, colors are time slots
Register allocation in compilers: Variables in a program are nodes, simultaneously live variables are edges, colors are CPU registers. This was the original motivation for graph coloring in CS
Frequency assignment in cell networks: Cell towers must use different frequencies if their coverage areas overlap — a classic graph coloring problem with billions of dollars in spectrum at stake
Map coloring in GIS: Geographic information systems use the four color theorem to render political maps with minimal color sets while keeping borders readable
Sudoku: The game is essentially a graph coloring problem on a 9×9 Latin square graph with 9 colors

← Back to all ciphers