Four Color Theorem

Theorem

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

Also known as

In British English, this theorem is spelled four colour theorem.

Some sources continue to refer to it as the four colo(u)r problem, acknowledging the controversial nature of its supposed proof.

Historical Note

The question of the minimal number of colors that are needed to color any arbitrary planar graph was first considered by Francis Guthrie in $1852$, when he was coloring a map of the counties of England.

He conjectured that the answer was $4$.

He published this conjecture in $1878$.

In $1879$, Alfred Bray Kempe published what he believed to be a proof, but in $1890$ it was shown by Percy John Heawood to be flawed.

In that same year, Heawood proved that $5$ colors were certainly enough.

In $1880$, another proof was published, but that was also shown to be flawed.

During the course of the century following, many developments in graph theory were made as a result of research into this problem.

What is now believe to be a sound proof of the Four Color Theorem was presented in $1976$ by Kenneth Ira Appel and Wolfgang Haken.

Their proof relies heavily on a computer program, set up to search through all the various cases.

Hence their proof does not easily conform to $\mathsf{Pr} \infty \mathsf{fWiki}$'s format.

Apart from this computer-based search, the proof is similar to that of the Five Color Theorem, a related but weaker result.

Some mathematicians distrust this proof because of its reliance on computers, and its consequent inability to be checked by humans.

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