Further Reading: Graph Coloring, Planarity, and the Four Color Theorem

Annotated pointers for going deeper. Start with the textbook sections to firm up the core, then branch toward whatever pulls you: the story of the Four Color Theorem, the systems application (register allocation), or the theory (Kuratowski, planarity testing).

Core textbook treatments

Rosen, Discrete Mathematics and Its Applications (8th ed.), §10.7 (Planar Graphs) and §10.8 (Graph Coloring) The market-standard treatment, with Euler's formula, the edge bounds, Kuratowski's theorem, the chromatic number, and the Four Color Theorem stated and discussed. A large, well-graded exercise bank — the place to go for more drill than this chapter provides.

Lehman, Leighton & Meyer, Mathematics for Computer Science (MIT 6.042), the graph-coloring and planarity material Freely available. The most CS-flavored presentation in print: coloring is developed alongside its applications (scheduling, conflict resolution) in exactly the "why a programmer needs this" spirit of this chapter, with clean proofs of the greedy bound and the bipartite characterization.

West, Introduction to Graph Theory (2nd ed.), the chapters on coloring and planarity The standard upper-undergraduate graph-theory text. Rigorous, complete proofs of Euler's formula, the edge bounds, Kuratowski's theorem, and Brooks' theorem (a sharpening of the $\Delta+1$ bound this chapter mentions only as $\chi \le \Delta+1$). Go here when you want the full theory, not just the survey.

Levin, Discrete Mathematics: An Open Introduction (3rd ed.), the coloring and planar-graphs sections Freely available. A gentle, exercise-rich open textbook. Its planarity and coloring sections pair well with this chapter for a second explanation in plainer language, with many small worked examples.

On the Four Color Theorem — the story and the controversy

Robin Wilson, Four Colors Suffice: How the Map Problem Was Solved The definitive popular history: Guthrie's 1852 conjecture, Kempe's flawed 1879 "proof," Heawood's 1890 correction (and the five-color theorem), and the 1976 Appel–Haken computer proof. Read this for the human story behind §33.5 and the threshold-concept discussion of computer-assisted proof.

Appel & Haken, "Every Planar Map is Four Colorable" (the 1976 announcement and the Illinois Journal of Mathematics papers) Tier 2 — attributed. The original proof. Not light reading, but worth seeing the shape of it: an "unavoidable set" of reducible configurations checked by computer. Skim it to understand why no human could verify every case by hand — the crux of the philosophical debate.

Gonthier, "Formal Proof — The Four-Color Theorem" (Notices of the AMS, 2008) Tier 2 — attributed. A readable account of the 2005 fully machine-checked proof in the Coq proof assistant (Gonthier and Werner). The natural follow-up to Wilson's history: it explains how the trust moved from "a one-off program" to "a small, scrutinized proof-checking kernel," without removing the computer from the loop.

On the systems payoff — register allocation

Cormen, Leiserson, Rivest & Stein (CLRS), Introduction to Algorithms (4th ed.), the graph chapters Background on graph representations and traversals that the coloring algorithms here build on. CLRS does not cover register allocation per se, but its graph machinery is the foundation.

Chaitin et al., "Register Allocation via Coloring" (the foundational graph-coloring-allocation work) Tier 2 — attributed. The classic paper that framed register allocation as graph coloring of the interference graph — exactly the model of §33.2 and Case Study 1. The origin of every coloring-based allocator in GCC and LLVM. Seek it out to see the theory of this chapter become a production compiler pass.

Videos and visual intuition

Numberphile, the Four Color Theorem / map-coloring episodes (YouTube) Free. Short, accessible video tellings of the four-color story and why four colors suffice, with the "three houses, three utilities" ($K_{3,3}$) puzzle. Good for building the why before the proofs.

3Blue1Brown, planar-graph and Euler's-formula explainers (YouTube) Free. Visual intuition for $V - E + F = 2$ and the polyhedron connection (§33.3's Connection callout). Helpful if the face-counting double-count still feels abstract.

Suggested order

  1. Re-read §§33.1–33.3 here, then do Rosen §10.7–10.8 exercises for drill on Euler's formula and the chromatic number.
  2. Read the MIT 6.042 coloring material for the CS framing and the scheduling/conflict applications.
  3. Read Wilson's Four Colors Suffice (or watch the Numberphile episode first) for the §33.5 story, then Gonthier's Notices article for the formal-proof epilogue.
  4. For the systems thread, read CLRS's graph chapters, then the Chaitin register-allocation paper alongside Case Study 1.
  5. Save West's coloring/planarity chapters for when you want complete proofs of Kuratowski's theorem and Brooks' theorem beyond this chapter's scope.