The Four Color Theorem: Four Colors Suffice for Every Planar Map

What the theorem says, and the fine print hiding in the word "map"

A map here means a finite subdivision of the plane (or the sphere) into regions by simple closed curves. A proper coloring assigns a color to each region so that regions sharing a boundary arc get different colors. The theorem: four colors always suffice.

Three hypotheses do real work, and dropping any of them kills the result:

• Each region is connected. If a country may consist of several separate pieces that must all take the same color, four colors are hopeless. For countries with at most m pieces the sharp answer is 6m colors for every m ≥ 2 (Heawood's bound of 1890, shown tight by Jackson and Ringel in 1984) — so two-piece countries already need twelve.
• Adjacency means a shared arc, not a shared point. Cut a disc into n pie slices and every slice touches every other at the center. If point contact counted as adjacency, that map would need n colors for any n you like. The standard convention excludes it: the slices then form a cycle Cₙ, which needs only 2 colors when n is even and 3 when n is odd.
• The surface is the plane or the sphere. These two cases are the same problem: stereographic projection turns a sphere map into a plane map and back, with one region becoming the unbounded outer face. On a torus the answer is seven, not four.

The graph-theoretic form is the one mathematicians actually prove: every planar graph — a graph drawable in the plane with no edge crossings — has chromatic number at most 4. Loops make a graph uncolorable and are excluded; parallel edges are irrelevant since they impose the same constraint twice.

Maps become graphs: the dual construction

Put a vertex inside every region. Whenever two regions share a boundary arc, join their vertices by an edge drawn across that arc. The result is the dual graph of the map, and because each edge can be drawn through the border it represents, the dual is drawn without crossings: it is planar.

This turns a statement about areas into a statement about vertices, and it is an exact translation, not an analogy. A proper coloring of the map is literally a proper coloring of the dual graph and vice versa. Conversely, every planar graph arises this way — a planar embedding of G has a dual map whose regions correspond to G's vertices — so the map theorem and the graph theorem are equivalent.

The reduction also lets you normalize the problem. It is enough to prove the theorem for simple planar triangulations (every face a triangle): adding edges only makes coloring harder, so if every maximal planar graph is 4-colorable, every planar graph is. Every modern proof works with triangulations, because Euler's formula is sharpest there: a triangulation on V ≥ 3 vertices has exactly E = 3V − 6 edges and F = 2V − 4 faces.

Why three colors fail: the five-wheel, and what the picture proves

Take a region ringed by five others — the graph is the wheel W₅, a hub joined to every vertex of a 5-cycle. Try three colors. The rim is C₅, an odd cycle, so it cannot be 2-colored: going red, blue, red, blue around the ring, the fifth region touches both a red and a blue neighbor and is forced onto the third color. Now every one of the three colors appears on the rim, and the hub touches all five rim regions. No color is left. Since three colors were available and a proper coloring still failed by force — not by bad luck — W₅ has χ = 4.

The smallest example is even simpler: K₄, four mutually adjacent regions, which is planar and obviously needs four colors. Both examples prove the lower bound: four colors are sometimes necessary. That is all a picture can do. The upper bound — four colors are always enough, for every one of the infinitely many planar maps — is the theorem, and no diagram establishes it. Any explainer that shows a map failing at three colors and then succeeding at four has demonstrated necessity and illustrated sufficiency; the sufficiency is what took 124 years.

The asymmetry has a sharp computational shadow. Deciding whether a given planar graph is 3-colorable is NP-complete, proved by Garey, Johnson and Stockmeyer in 1976 — the same year as the main theorem — and it stays NP-complete for planar graphs of maximum degree 4. Deciding 4-colorability of a planar graph, by contrast, is trivial: the answer is always yes. Grötzsch's theorem (1959) carves out the well-behaved case: every triangle-free planar graph is 3-colorable.

The easy half: Euler's formula, five colors, and Kempe's broken chain

Everything starts with Euler's formula V − E + F = 2 for a connected planar graph. Counting incidences, each face of a simple planar graph is bounded by at least 3 edges and each edge borders at most 2 faces, so 2E ≥ 3F; substituting gives E ≤ 3V − 6 for V ≥ 3. Since the degrees sum to 2E ≤ 6V − 12, the average degree is below 6, so every planar graph has a vertex of degree at most 5. That single corollary is the foothold for every attack on the problem.

It yields the five color theorem in about a page. Take a minimal counterexample, pick a vertex v of degree ≤ 5, color G − v by minimality, and put v back. If v's neighbors use at most 4 colors, recolor v with the fifth and finish. Otherwise v has exactly five neighbors in five distinct colors; choose two non-adjacent neighbors a (color 1) and b (color 3) and look at the Kempe chain: the connected component containing a of the subgraph induced by colors 1 and 3. If b is not in it, swap colors 1 and 3 throughout that component — a still-proper coloring in which color 1 is freed for v. If b is in it, the 1–3 chain from a to b together with v encloses one of the other neighbors, so its own 2–4 chain cannot escape, and the swap works there instead. Planarity is doing the work: the Jordan curve theorem is what forbids the two chains from crossing.

Alfred Kempe published exactly this argument in 1879 and claimed it also handled four colors. For the degree-5 case he performed two Kempe interchanges at once. Percy Heawood found the flaw in 1890: the two chains can interfere, and the second swap can undo the first. Heawood salvaged the five color theorem — which is what Kempe's method really proves — and the four color problem was open again. Peter Guthrie Tait's 1880 proof failed too, but his reduction survives: the four color theorem is equivalent to the statement that every bridgeless cubic planar graph is 3-edge-colorable.

Unavoidability and reducibility: the machine at the heart of the 1976 proof

The winning strategy, developed by George Birkhoff (1912) and industrialized by Heinrich Heesch in the 1960s, is to find a finite list of local pictures with two properties. A set of configurations is unavoidable if every planar triangulation contains at least one of them. A configuration is reducible if a minimal counterexample cannot contain it — that is, any 4-coloring of the smaller graph obtained by contracting it can be massaged, via Kempe chains, into a coloring of the whole. An unavoidable set of reducible configurations proves the theorem, because a minimal counterexample would have to contain something it cannot contain.

Unavoidability is proved by discharging. In a triangulation, give each vertex the charge 6 − deg(v); Euler's formula makes the total charge exactly 12, hence positive, since Σ(6 − deg v) = 6V − 2E = 6V − 2(3V − 6) = 12. Now push charge around by fixed local rules — for instance, every vertex of degree ≥ 7 sends a fixed fraction of its charge to each neighboring degree-5 vertex. If no configuration from the list occurs, one shows every vertex ends with charge ≤ 0, contradicting the positive total. Heesch estimated that around 8,900 configurations would be needed and could not finish the computation.

Appel and Haken, with John Koch handling much of the reducibility code, closed it in June 1976 with an unavoidable set of 1,936 reducible configurations (later trimmed to 1,476), verified with roughly 1,200 hours on an IBM 360 at the University of Illinois. The reducibility test for a configuration explores the 4-colorings of its bounding ring — rings ran up to size 14, so the search spaces are large but finite. The results appeared in 1977 as two papers in the Illinois Journal of Mathematics, "Part I: Discharging" and "Part II: Reducibility"; the Urbana postmark read FOUR COLORS SUFFICE. In 1997 Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas published an independent, leaner proof: 633 configurations and 32 discharging rules, plus a quadratic-time O(n²) algorithm that actually outputs a 4-coloring, where the Appel–Haken machinery gave a quartic one.

A proof no human has read: surveyability and the Coq verification

The 1976 proof provoked a genuine philosophical argument rather than mere grumbling. Thomas Tymoczko argued in the Journal of Philosophy (1979) that the four color theorem introduced an empirical, a posteriori element into mathematics: nobody can check 1,936 reducibility computations by hand, so acceptance rests partly on trusting hardware and code. The practical worry was not idle. Appel and Haken's discharging argument required corrections; Ulrich Schmidt's 1981 independent check of part of it turned up errors, all repairable, and the 1989 monograph Every Planar Map Is Four Colorable shipped with a several-hundred-page appendix of corrections and microfiche.

The verification worry was answered in 2005, when Georges Gonthier, with Benjamin Werner, produced a complete formal proof in the Coq proof assistant — roughly 60,000 lines, covering both the combinatorial core and the computational checks, published in the Notices of the AMS in 2008. Everything now rests on the small, heavily scrutinized Coq kernel rather than on ad hoc C programs, and the formalization forced a cleaner combinatorial framework (hypermaps) along the way.

What has not happened, as of 2026, is a short proof. No argument is known that a mathematician can read end-to-end and understand why four colors suffice. The theorem is certain and unilluminating, and it remains the standard example in debates about what a proof is for: certification, or explanation.

Off the plane: seven colors on a doughnut, and what four colors is not good for

Counterintuitively, harder surfaces were settled first. Heawood's 1890 paper — the one that demolished Kempe — also proved that a map on an orientable surface of genus g ≥ 1 needs at most H(g) = ⌊(7 + √(1 + 48g))/2⌋ colors. For the torus, g = 1 gives 7, and K₇ embeds in the torus, so seven is exactly right. Proving the bound is attained for every g ≥ 1 was the Heawood conjecture, settled by Gerhard Ringel and J. W. T. Youngs in 1968. The non-orientable analogue has exactly one exception: the Klein bottle takes 6, not the formula's 7, as Philip Franklin showed in 1934. The formula itself gives H(0) = 4, the right answer — but Heawood's argument needs g ≥ 1, so the plane is exactly the case his proof cannot reach, and that case is the four color theorem itself.

Several famous statements are equivalent to, or implied by, the theorem. Hadwiger's conjecture for k = 5 is equivalent to it (Wagner, 1937); the k = 6 case was proved by Robertson, Seymour and Thomas in 1993 using the four color theorem itself, and the general conjecture is open. Tait's equivalence means the theorem is the same as "no planar snark exists." Louis Kauffman gave a reformulation in terms of the vector cross product in 1990.

Applications are worth being honest about. The theorem is routinely advertised as underpinning frequency assignment, register allocation in compilers, or scheduling — and it does not, because those conflict graphs are not planar, and for general graphs computing χ(G) is NP-hard and even hard to approximate. The real legacy is methodological: discharging became a standard tool of structural graph theory, powering results such as Grötzsch's theorem and the 2017 disproof of Steinberg's conjecture by Cohen-Addad, Hebdige, Král', Li and Salgado. And the RSST algorithm does deliver something concrete — a guaranteed 4-coloring of any planar graph in quadratic time.

Four is the answer only for connected regions on a flat plane or a sphere. Change the surface or the definition of a country and the number changes with it.

Setting	Colors always enough	Colors sometimes needed	Settled by
Plane or sphere, each region connected	4	4 — K₄ and the five-wheel W₅ force it	Appel & Haken 1976; Robertson–Sanders–Seymour–Thomas 1997
Plane, triangle-free map (no three regions mutually adjacent)	3	3 — the 5-cycle C₅ forces it	Grötzsch 1959
Torus (doughnut)	7	7 — K₇ embeds in the torus	Heawood 1890 (bound); Ringel & Youngs 1968 (tight)
Klein bottle	6	6	Franklin 1934 — the single exception to Heawood's formula
Plane, countries with up to m separate pieces (m ≥ 2)	6m	6m — tight for every m ≥ 2	Heawood 1890 (bound); Jackson & Ringel 1984 (tight)