Four colour theorem

Statement

Let $G$ be a finite loopless planar graph. Then $\chi(G) \le 4$.

Remarks

In terms of maps: four colours are enough for the regions of a map in the plane. Regions with a common boundary segment get different colours. The bound is sharp, because $K_4$ is planar and $\chi(K_4) = 4$.

History

Francis Guthrie stated the problem in 1852. Kenneth Appel and Wolfgang Haken proved the theorem in 1976, with the help of a computer. Robertson, Sanders, Seymour and Thomas gave a simpler proof in 1997. Georges Gonthier and Benjamin Werner checked a proof in the Coq proof assistant in 2005.

Explanations

L1 human

Four colours are enough to colour any map, so that neighbouring countries always have different colours. It was the first major theorem whose proof needed a computer.