Worked solution: Appel–Haken discharging proof with computer-verified reducibility (1976)
Draw one dot inside each country of a map and connect two dots with a line whenever their countries share a border; the map-colouring question — can every map be coloured with just colours so neighbours differ — becomes the question of colouring the dots of this graph so that connected dots never share a colour.
To prove no map ever needs a th colour, mathematicians imagine the opposite: suppose some map somewhere does need colours, and among all such troublesome maps pick the very smallest one. If that assumption leads to a contradiction, no such map can exist at all — a classic proof strategy called a minimal counterexample.
Represent each map as a planar graph (one vertex per region, edges between adjacent regions); the claim to prove becomes , where is the chromatic number, the fewest colours needed so that no edge joins two same-coloured vertices.
Following the strategy pioneered by Alfred Kempe (1879) and corrected by Percy Heawood (1890), assume for contradiction that a counterexample exists — some planar graph needing colours — and, among all counterexamples, pick a minimal one : the smallest planar graph (by number of vertices) with . Every proper subgraph of then has , since it is smaller.
This minimal counterexample is the object every later step studies. If it can be shown that no such graph can actually exist, the four colour theorem follows immediately.
- Chromatic number
- The fewest number of colours needed to colour the vertices of a graph so that no edge joins two vertices of the same colour.
- Minimal counterexample
- Among all objects (here, planar graphs) that would violate a claimed theorem, the smallest one; used to derive a contradiction by showing it must contain a smaller counterexample too, which is impossible.