I have been studying planar graphs for a while now and found it useful for my learning to formulate a few proofs myself, based on the study material I worked through. This proof is about the 5-color Theorem. I was wondering if proof by induction or contradiction is better, but I decided for proof by induction, as this is easier to translate in actual code then.
Have a look at my proof, any feedback appreciated:
Lemma 1: Every planar graph contains a vertex with $\operatorname{deg}(v) \leq 5$.
Theorem: Every planar graph with $n$ vertices can be colored using at most 5 colors.
Proof by induction, we induct on $n$, the number of vertices in a planar graph $G$.
Base case, $P(n \leq 5)$: Since there exist $\leq 5$ nodes in $G$, the graph can be colored using 5 colors.
Inductive step, $P(n+1)$: Assuming $P(n)$ is true, that is, every planar graph with $n$ vertices, we need to show $P(n)$ is true.
By Lemma 1, we know every planar graph has one vertex with $\operatorname{deg}(v) \leq 5$. We call this vertex $v$ in our graph $G$. Remove $v$ and for the remaining subgraph $G'$ we can assume $P(n)$.
If $\operatorname{deg}(v) \leq 4$, we can color all vertices adjacent to $v$ using 4 colors and use color 5 to color $v$ itself to reach a valid coloring.
If $\operatorname{deg}(v) = 5$, we assume that all vertices adjacent to $v$ are colored in different colors.
Assume there exists no path from $A$ to $C$.
We can change the color of $A$ from red to blue, the color of $C$. Since no neighbor of $v$ now has the color red, we can color $v$ in red. We also need to change all vertices adjacent to $A$ from blue to red. Since no path exists from $A$ to $C$, the color of $C$ remains unchanged.
Assume there exists a path from $A$ to $C$, alernating in color from red to blue. Note that this path bounds a planar embedding with $B$ on the inside and $D$ on the outside.
We can change the color of $B$ from green to yellow, the color of $D$. Since no neighbor of $v$ now has the color green, we can color $v$ in green. We also need to change all vertices adjacent to $B$ from yellow to green. Since no path can exist from $B$ to $D$ (without crossing the path from $A$ to $C$), the color of $D$ remains unchanged.
Best Answer
You use all the right ideas, but should be more exacty in the elaborations. For example, you swithch from "no path (at all)" to "exists a path ... alternating in color", and in general, it will not suffice to change the colour of $A$ alone.
More strictly, we consider the graph $G'$ obtained by removing $v$ (and its incident edges) from $G$. By induction hypothesis, $G'$ can be 5-coloured. We consider a valid 5-colouring of $G'$ and modify it, if necessary,, toachieve a 5-colouring of $G$.
For the $\deg(v)=5$ case, instead of paths from $A$ to $C$ etc., you may want to consider "red-blue" (and "green-yellow") components, i.e., connected subgraphs of $G'$ where all vertices are red or blue (according to the colouring of $G'$ we picked). If $A$ and $C$ are not in the same red-blue component, we can win by flipping all colours red$\leftrightarrow$blue in the component of $A$, say. Whereas if $A$ and $C$ are in the same red-blue component, we find a red-blue path from $A$ to $C$ in $G'$ which - together with $v$ - forms a closed Jordan curve separating $B$ from $D$. As red-blue paths and green-yellow paths cannot intersect, we conclude that $V$ and $D$ are not in the same green-yellow component and we win by flipping all vertex colours green$\leftrightarrow$yellow in the component of $B$, say.