We formalize the classical six color theorem: every finite planar graph admits a proper vertex coloring with six colors. Planarity is taken to mean the existence of a crossing-free straight-line drawing in the plane. The proof follows the textbook route. Euler's formula $v - e + f = 2$ for connected plane graphs gives the edge bound $e \leq 3v - 6$. This bound yields a vertex of degree at most $5$, and induction on the number of vertices completes the coloring.