Four Color Theorem Paper
James Pfeiffer (Math 581d Fall 2010 University of Washington)

history

The Four Color Theorem (4ct) was the first mathematical theorem with a
computer proof. It was conjectured in 1852 and proved in 1976. Since
then there has been additional work on the theorem.

appel proof

In 1976 Appel and Haken announced a proof of the theorem. Their proof
exhibited an unavoidable set of configurations which are reducible -
thus they must appear in any minimal counterexample, but any minimal
counterexample containing them can be made smaller. Their proof has
never been completely checked.  An interesting result of this proof
was the existence of a quartic-time algorithm for producing a coloring
of a planar graph.

thomas proof

In 1996 Neil Robertson, Daniel P. Sanders, Paul Seymour and Robin
Thomas gave a streamlined proof of the theorem. They streamlined the
reducibility part of the proof.  More importantly, they implemented a
computer proof of the unavoidability part as well: in the 1976 proof
this was contained in 400 pages of microfiche. The new proof uses two
lemmas which are each verified by running a computer program. Assuming
the validity of the lemmas, the rest of the proof is quite short and
resembles a standard mathematical paper.  Another consequence of this
work was the improvement of the quartic algorithm above to a
quadratic-time one.

gonthier proof

In 2005 Gonthier implemented the entire proof of the theorem in the
Coq automated theorem checker. This required defining many terms, eg
planar graph, formally and in a way that could be used in Coq. The
necessity of formalizing these terms led Gonthier to some new
mathematics, in addition to the goal of formalizing the theorem.

further work

There are still open questions relating to the 4ct. Recently
Steinberger proved that there is an unavoidable set of D-reducible
configurations.  The reducible configurations used in all proofs so
far fall into two categories: "C-reducible" or "D-reducible". The
C-reducible configurations are more delicate to test for reducibility,
and so the existence of a set using only D-reducible configurations
led to a further simplification of the proof. Although there seems to
be no hope for a "computer-less" proof of the theorem, such as exists
for the five-color theorem, there may be more such simplifications
possible.  It isn't known whether the O(n^2) algorithm for
four-coloring planar graphs is optimal; perhaps there is a linear-time
algorithm.  In another direction, the Hadwiger conjecture in graph
theory is a generalization of the four-color theorem in terms of graph
minors.

citations

http://en.wikipedia.org/wiki/Four_color_theorem
http://people.math.gatech.edu/~thomas/FC/fourcolor.html
http://www.ams.org/notices/199807/thomas.pdf
http://www.ams.org/notices/200811/tx081101382p.pdf