[proofplan] We argue by strong induction on $n := |G|$. The base case $n \leq 6$ is immediate: colour each vertex with a distinct colour from the palette $\{1, \ldots, 6\}$. For $n \geq 7$, the [Minimum Degree of Planar Graphs](/theorems/2026) theorem produces a vertex $x \in V(G)$ of degree at most $5$. The induced subgraph $G - x$ is planar with $|G - x| = n - 1$, so by induction it admits a proper $6$-colouring. Since $x$ has at most $5$ neighbours, some colour from the palette is not used by any neighbour of $x$; extend the colouring by assigning this free colour to $x$. [/proofplan]

[step:Set up strong induction on the number of vertices]Let $P(n)$ be the statement: **every planar graph $G$ with $|G| = n$ satisfies $\chi(G) \leq 6$.** We prove $P(n)$ for all $n \geq 0$ by strong induction on $n$.[/step]

[guided]Strong induction on $|G|$ is the natural inductive parameter because the Minimum Degree of Planar Graphs theorem guarantees that in any planar graph with $\geq 3$ vertices we can find a low-degree vertex $x$ to remove; this reduces the problem to a smaller planar graph $G - x$, to which the inductive hypothesis applies. Removing a vertex decreases $|G|$ by exactly $1$, but the argument becomes cleanest if we allow the inductive hypothesis to apply to all smaller planar graphs (not just $|G| - 1$), since this lets us handle base cases of varying sizes uniformly.[/guided]

[step:Handle the base cases $n \leq 6$]Suppose $n \leq 6$ and let $G$ be a planar graph with $|G| = n$. Define the colouring \begin{align*} c: V(G) &\to \{1, 2, \ldots, n\} \subseteq \{1, \ldots, 6\}, \\ v_i &\mapsto i, \end{align*} where $v_1, \ldots, v_n$ is any enumeration of $V(G)$. Since all $n$ colour values are distinct, $c$ is injective, so in particular $c(u) \neq c(v)$ for every edge $uv \in E(G)$ (with $u \neq v$ because $G$ is simple). Hence $c$ is a proper $6$-colouring and $\chi(G) \leq n \leq 6$.[/step]

[guided]For $n \leq 6$ we have enough colours to give every vertex its own colour. A proper colouring requires $c(u) \neq c(v)$ only on edges, so injectivity (a stronger property) is certainly sufficient. For $n = 0$ the colouring is the empty map, immediately proper (there are no edges to check), and $\chi(G) = 0 \leq 6$. This covers $n = 0, 1, 2, 3, 4, 5, 6$, giving the base cases of the induction.[/guided]

[step:Extract a low-degree vertex via the planar minimum degree bound]Let $n \geq 7$ and assume the inductive hypothesis: $P(m)$ holds for every $0 \leq m < n$. Let $G$ be a planar graph with $|G| = n \geq 7 \geq 3$. By the [Minimum Degree of Planar Graphs](/theorems/2026) theorem, \begin{align*} \delta(G) \leq 5, \end{align*} so there exists a vertex $x \in V(G)$ with $\deg_G(x) \leq 5$. Fix one such $x$.[/step]

[guided]The Minimum Degree of Planar Graphs theorem requires $|G| \geq 3$. We have $n \geq 7$, which comfortably satisfies this hypothesis. The conclusion is that there is at least one vertex of degree at most $5$; we choose one and call it $x$. Why degree at most $5$ and not, say, at most $4$? The bound $\delta(G) \leq 5$ is tight (e.g., for the icosahedron, every vertex has degree exactly $5$). This is precisely why the Six-Colour Theorem uses $6$ colours and not $5$: with $5$ neighbours at $x$, we need $6$ colours in the palette to guarantee one is free.[/guided]

[step:Apply the inductive hypothesis to $G - x$ and extend to a $6$-colouring of $G$]Consider the induced subgraph $G - x$ obtained by deleting the vertex $x$ and all edges incident to it. Since $G$ is planar and $G - x$ is an induced subgraph, $G - x$ is also planar (a plane embedding of $G$ restricts to a plane embedding of $G - x$). Moreover \begin{align*} |G - x| = n - 1 < n, \end{align*} so by the inductive hypothesis $P(n - 1)$, there is a proper $6$-colouring \begin{align*} c': V(G - x) &\to \{1, 2, 3, 4, 5, 6\}, \\ v &\mapsto c'(v). \end{align*} Let $N(x) = \{y_1, \ldots, y_d\}$ be the neighbourhood of $x$ in $G$, where $d = \deg_G(x) \leq 5$. The set of colours already used by neighbours of $x$ under $c'$ is \begin{align*} F := \{c'(y_j) : 1 \leq j \leq d\}, \end{align*} and satisfies $|F| \leq d \leq 5 < 6 = |\{1, \ldots, 6\}|$. Hence $\{1, \ldots, 6\} \setminus F \neq \varnothing$; pick any $c_0 \in \{1, \ldots, 6\} \setminus F$. Define \begin{align*} c: V(G) &\to \{1, 2, 3, 4, 5, 6\}, \\ v &\mapsto \begin{cases} c'(v) & \text{if } v \neq x, \\ c_0 & \text{if } v = x. \end{cases} \end{align*} We verify $c$ is proper. Let $uv \in E(G)$. There are two cases: - $u, v \neq x$: then $uv \in E(G - x)$, so $c(u) = c'(u) \neq c'(v) = c(v)$ by properness of $c'$. - Exactly one of $u, v$ equals $x$: say $v = x$ and $u \in N(x)$. Then $c(u) = c'(u) \in F$ while $c(x) = c_0 \notin F$, so $c(u) \neq c(x)$. (The case $u = v = x$ does not occur because $G$ is simple.) Hence $c$ is a proper $6$-colouring of $G$, giving $\chi(G) \leq 6$. This establishes $P(n)$ and completes the induction.[/step]

[guided]The inductive step has three parts: (i) verify $G - x$ is planar of smaller size, (ii) invoke the inductive hypothesis to $6$-colour $G - x$, and (iii) extend the colouring to $x$ using a free colour. For (i): $G - x$ is an induced subgraph of $G$. Planarity is preserved by taking induced subgraphs because deleting vertices and their incident edges in a plane drawing still leaves a plane drawing. And $|G - x| = n - 1 < n$. For (ii): by inductive hypothesis $P(n-1)$, any planar graph of size $n - 1$ has chromatic number at most $6$. So there is a proper colouring $c': V(G - x) \to \{1, \ldots, 6\}$. For (iii): we need to extend $c'$ by choosing $c(x)$ so that the extension is still proper. The only new edges to worry about are $x y_j$ for $y_j \in N(x)$, which require $c(x) \neq c'(y_j)$. The forbidden colours form a set $F = \{c'(y_j) : y_j \in N(x)\}$ of size at most $\deg_G(x) \leq 5$. Since the palette has $6$ elements, $\{1, \ldots, 6\} \setminus F$ is non-empty. Pick any $c_0$ in this set and assign $c(x) = c_0$. Why does edge-properness hold for edges not incident to $x$? Because on $V(G - x)$ the colouring $c$ coincides with $c'$, which was already proper on $G - x$. So all old edges are fine, and all new edges ($x y_j$) are handled by the choice $c_0 \notin F$.[/guided]