Four Color Theorem

Theorem

Any planar graph $G \ $ can be assigned a proper vertex $k$-coloring such that $k \le 4$.

Proof

A proof of this was provided in 1976 by Kenneth Appel and Wolfgang Haken. However, their proof relies heavily on computers, meaning that it is not something that would easily conform to ProofWiki's format. Outside of the portion necessitating computers, the proof is similar to that of the Five Color Theorem, a related but weaker result.

Controversy

There are some mathematicians who dislike this proof because of its reliance on computers, and therefore its inability to be checked by humans.

This is part of a broader debate in mathematics over the increasing use of computers in proofs.