5-Coloring Planar Graphs with a Color Class of Order at Most $\mathrm{\mid }V\mathrm{\mid }\mathrm{/}6$

We show that any planar graph $G=(V,E)$ has a 5-coloring such that one color class contains at most $\mathrm{\mid }V\mathrm{\mid }\mathrm{/}6$ vertices. In other words, there exists a partition of $V$ into five independent sets $\{V_1,\cdots ,V_5\}$ such that $\mathrm{\mid }{V}_5\mathrm{\mid }\le \mathrm{\mid }V\mathrm{\mid }\mathrm{/}6$. Our proof yields an $O(\mathrm{\mid }V{\mathrm{\mid }}^2)$-time algorithm to find such a partition, and unlike the Four Color Theorem, our proof is fully verifiable without computer assistance.