Grötzsch's theorem

Remarks

An easy weaker bound comes from Euler's formula. A triangle-free planar graph with $n \ge 3$ vertices has at most $2n - 4$ edges, so it has a vertex of degree at most $3$. Induction then gives a colouring with $4$ colours. Getting down to $3$ colours needs a finer induction, which proves a stronger statement about extending colourings from a short precoloured face. Herbert Grötzsch proved the theorem in 1959, and Carsten Thomassen later gave shorter proofs. Both hypotheses are needed. Without the triangle condition the bound fails: $K_4$ is planar and needs $4$ colours. Without planarity it fails too: the Grötzsch graph, with $11$ vertices, is triangle-free and needs $4$ colours. For example, every planar bipartite graph is triangle-free, and indeed $2$-colourable.

Going deeper

For a student

The theorem is a sharp statement about the interplay of girth and colouring on surfaces. Grünbaum and Aksenov extended it to planar graphs with at most three triangles. The precoloured-face strengthening used in the proof is typical of colouring proofs for planar graphs, as in the proof that planar graphs are $5$-choosable.