It is obvious that the chromatic number of any complete graph $K_n$ corresponds to the number $n$ of its vertices since each of its vertices is adjacent to any other vertex. Therefore, it has to be colored with a distinct color. With a growing $n$, the chromatic number of the complete graph $K_n$ is unbounded. It is, therefore, natural to conjecture that the more complicated a graph is, the more colors are needed to color its vertices.
It turns out that this conjecture is false for planar graphs graphs. In fact, planar graphs, no matter how complicated they are, are $k$-colorable with a small and surprisingly finite chromatic number.
The $k$-colorability of planar graphs led to a famous mathematical conjecture, the 4-color conjecture that was first formulated in the 19th century and stated that any planar graph has a chromatic number of 4. This conjecture turned out to be extremely hard to prove or disprove. Finally, a computer-assisted proof was provided in 1976, and it is so complicated that humans can only verify the correctness of the proving algorithm, but not the proof itself. With this respect, this proof remains highly unsatisfactory for mathematicians.
In this chapter, we will provide some basic results about coloring of planar graphs, including the 4-color theorem.
