The proof of the four color theorem for planar graphs found in 1976 was computer-assisted. Due to its complexity, it cannot be directly verified by humans. Only the validity of the proving computer algorithm can be verified. This is a highly unsatisfactory situation for mathematicians. In fact, some mathematicians do not accept computer-assisted proofs as mathematical proofs.
The following theorem is a direct implication of the characterization of planar hamiltonian graphs proved by me in 2014. To my knowledge (as of 2020) it is also one of only a few strict proofs of a special instance of the 4-color theorem, which can be verified by humans.
Let $G$ be a simple, connected, planar graph. If the dual graph $G^*$ is Hamiltonian, then the chromatic number of $G$ obeys the following inequality $$\chi(G)\le 4.$$