Every planar graph can be colored with at most 4 colors such that no two adjacent regions share a color. Proved by Appel & Haken (1976) using computer assistance — the first major theorem proved by computer.
Select Color
Graph Stats
Vertices: -
Edges: -
Colors used: -
Conflicts: -
Status: -
Instructions
Click a vertex to color it
with the selected color.
Greedy: assign lowest
available color greedily.
Backtrack: find a valid
4-coloring by backtracking.
Try to color manually
with just 4 colors!
Four-Color Theorem (Appel-Haken 1976, Robertson-Sanders-Seymour-Thomas 1997): Every planar graph is 4-colorable. The proof reduces to checking ~633 unavoidable configurations by computer. It remains controversial as no purely human-verifiable proof exists. Graph coloring is NP-complete in general (3-coloring is NP-complete even for planar graphs).