Worked solution: Appel–Haken discharging proof with computer-verified reducibility (1976)

Every map gives a planar graph by duality: place one vertex inside each region of the map and join two vertices by an edge whenever their regions share a boundary edge. The map is four-colourable exactly when this dual graph $G$ satisfies $\chi(G) \le 4$, where $\chi(G)$ is the chromatic number — the least number of colours in a proper vertex-colouring. Loops never arise (no region borders itself) and parallel edges may be collapsed to one without affecting colourability, so $G$ may be taken to be a simple planar graph.

Assume the theorem fails and choose a counterexample $G$ with the fewest vertices: the well-ordering of the natural numbers guarantees such a $G$ exists whenever any counterexample does. Minimality is the engine of the whole argument — every proper subgraph or contraction of $G$ is smaller, hence four-colourable, and every later step exploits this by colouring a smaller graph and then repairing the colouring over the removed part. It also explains why $G$ can be neither too sparse nor too rigid: $K_5$ is nonplanar, so $G$ cannot simply be a clique obstruction, and planarity forces $G$ to contain the low-degree structure studied in the next step.

The strategy — assume a minimal counterexample and show its supposedly unavoidable substructures are all reducible — descends from Kempe's 1879 attempt (whose error Heawood exposed in 1890) and was developed by Birkhoff and then Heesch, who coined the notions of unavoidable set and reducibility that Appel and Haken carried to completion in their 1977 Illinois Journal of Mathematics paper.