Four Color Theorem

From ProofWiki
Jump to navigation Jump to search

Theorem

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


Proof




Also known as

In British English, the Four Color Theorem is spelled Four Colour Theorem.

Some sources hyphenate: Four-Colo(u)r Theorem.

Some sources continue to refer to it as the Four Colo(u)r problem (with or without the hyphen), acknowledging the controversial nature of its supposed proof.


Also see


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.

Henry Ernest Dudeney, writing about it in a $1926$ publication, also drops the names of Augustus De Morgan, Arthur Cayley, Lothar Wilhelm Julius Heffter, Paul Wernicke, George David Birkhoff and Philip Franklin, and cites the work of Henry Roy Brahana before giving a (flawed) proof of his own.


What is now believed 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.


Sources