## An Approximate Restatement of the Four Color Theorem (Manuscript)

Authors: Atish Das Sarma, Amita Gajewar, Richard J. Lipton, Danupon Nanongkai

Journal:

Conference:

Abstract:

The celebrated Four Color Theorem was ﬁrst conjectured in the 1850’s. More than a century later Appel and Haken [1] were able to ﬁnd the ﬁrst proof. Previously, there had been many partial results, and many false proofs. Appel and Haken’s famous proof has one “drawback”: it makes extensive use of computer computation. More recently Robertson, Sanders, Seymour and Thomas [18] created another proof of the Four Color Theorem. However, their proof, while simplifying some technical parts of the Appel-Haken proof, still relies on computer computations.

There is some debate in the mathematical community about whether mathematicians should be satisﬁed with mathematical proofs that rely on extensive computation and there is interest in ﬁnding a new proof of the Four Color Theorem that relies on no computer computation. Such a proof would perhaps yield additional insights into why the Four Color Theorem is really true, and might yield new insights into the structure of planar graphs. In any case, there continues to be a search for such a proof.

The contribution of this paper is that we initiate a new approach towards proving the Four Color Theorem. Our approach is based on insights from computer science theory and modern combinatorics in the style of “Erd¨os”. Tait proved in 1880 [20] that the Four Color Theorem is equivalent to showing that certain plane graphs have edge 3-colorings. Our main result is that this can be weakened to show that if every one of these plane graphs has even an approximate edge 3-coloring, then the Four Color Theorem is true. While it is not clear that our approach will necessarily open new attacks on the Four Color Theorem, the connections made in this paper seem to be of independent interest.

Update History
[v1]
November 2007

The celebrated Four Color Theorem was ﬁrst conjectured in the 1850’s. More than a century
later Appel and Haken [1] were able to ﬁnd the ﬁrst proof. Previously, there had been many
partial results, and many false proofs. Appel and Haken’s famous proof has one “drawback”:
it makes extensive use of computer computation. More recently Robertson, Sanders, Seymour
and Thomas [18] created another proof of the Four Color Theorem. However, their proof, while
simplifying some technical parts of the Appel-Haken proof, still relies on computer computations.
There is some debate in the mathematical community about whether mathematicians should
be satisﬁed with mathematical proofs that rely on extensive computation and there is interest
in ﬁnding a new proof of the Four Color Theorem that relies on no computer computation. Such
a proof would perhaps yield additional insights into why the Four Color Theorem is really true,
and might yield new insights into the structure of planar graphs. In any case, there continues
to be a search for such a proof.
The contribution of this paper is that we initiate a new approach towards proving the Four
Color Theorem. Our approach is based on insights from computer science theory and modern
combinatorics in the style of “Erd¨os”. Tait proved in 1880 [20] that the Four Color Theorem is
equivalent to showing that certain plane graphs have edge 3-colorings. Our main result is that
this can be weakened to show that if every one of these plane graphs has even an approximate
edge 3-coloring, then the Four Color Theorem is true. While it is not clear that our approach
will necessarily open new attacks on the Four Color Theorem, the connections made in this
paper seem to be of independent interest.