**These pages are not updated anymore.
They reflect the state of
.
For the current production of this journal, please refer to
http://www.math.psu.edu/era/.
**

% ************************************************************************** % * The TeX source for AMS journal articles is the publisher's TeX code * % * which may contain special commands defined for the AMS production * % * environment. Therefore, it may not be possible to process these files * % * through TeX without errors. To display a typeset version of a journal * % * article easily, we suggest that you either view the HTML version or * % * retrieve the article in DVI, PostScript, or PDF format. * % ************************************************************************** % Author Package %% Translation via Omnimark script a2l, April 29, 1996 (all in one day!) %\controldates{16-JUL-1996,16-JUL-1996,16-JUL-1996,23-JUL-1996} \documentclass{era-l} \usepackage{amsthm,graphicx} %\issueinfo{2}{1}{}{1996} %% Declarations: \newtheoremstyle{pplain}% name of new theoremstyle {}% leave usual amount of space above {}% leave usual amount of space below {\itshape}% text is italic {}% indent the head 0pt {\bfseries}% print the heading bold {}% print . at the end of the head {.5em}% leave .5em space after the head {% \thmname{\bfseries(#1)} } \theoremstyle{pplain} \newtheorem*{theorem1}{2.1} %Theorem 2.1} \newtheorem*{theorem2}{2.2} %Theorem 2.2} \newtheorem*{theorem3}{2.3} \newtheorem*{theorem4}{3.1} \newtheorem*{theorem5}{4.1} \newtheorem*{theorem6}{4.2} \newtheorem*{theorem7}{4.3} \newtheorem*{theorem8}{4.4} %% User definitions: \renewcommand{\colon}{:} %\renewcommand{\list}[2]{\noindent \hangindent 3em\hangafter 1\hbox to 3em % {\hfil #1\quad }#2} \copyrightinfo{1996}{\ N.~Robertson, D.~P.~Sanders, P.~Seymour, R.~Thomas} \begin{document} \title{A new proof of the four-colour theorem} \author{Neil Robertson} \address{Department of Mathematics, Ohio State University, 231 W. 18th Ave., Columbus, Ohio 43210, \hbox{USA}} \email{robertso@math.ohio-state.edu} \thanks{Research partially performed under a consulting agreement with Bellcore, and partially supported by DIMACS Center, Rutgers University, New Brunswick, New Jersey 08903, USA\@.} \thanks{Neil Robertson was partially supported by NSF under Grant No. DMS-8903132 and by ONR under Grant No. N00014-92-J-1965.} \author{Daniel P. Sanders} \address{School of Mathematics, Georgia Institute of Technology, Atlanta, Georgia 30332, USA} \email{dsanders@math.ohio-state.edu} \thanks{Daniel P. Sanders was partially supported by DIMACS and by ONR under Grant No. N00014-93-1-0325.} \author{Paul Seymour} \address{Bellcore, 445 South Street, Morristown, New Jersey 07960, USA} \email{pds@bellcore.com} \author{Robin Thomas} \address{School of Mathematics, Georgia Institute of Technology, Atlanta, Georgia 30332, USA} \email{thomas@math.gatech.edu} \thanks{Robin Thomas was partially supported by NSF under Grant No. DMS-9303761 and by ONR under Grant No. N00014-93-1-0325.} \date{September 26, 1995} \subjclass{Primary 05C10, 05C15, 05C85} \commby{Ronald Graham} \begin{abstract}The four-colour theorem, that every loopless planar graph admits a vertex-colouring with at most four different colours, was proved in 1976 by Appel and Haken, using a computer. Here we announce another proof, still using a computer, but simpler than Appel and Haken's in several respects. \end{abstract} \maketitle \section*{1. Introduction } For our purposes a {\em graph} $G$ consists of a finite set $V(G)$ of vertices, a finite set $E(G)$ of edges, and an incidence relation between them. Each edge is incident with two vertices, called its {\em ends}. An edge whose ends are equal is called a {\em loop}. A {\em plane} graph is a graph embedded in the plane (without crossings, in the usual way). The four-colour theorem (briefly, the 4CT) asserts that every loopless plane graph admits a 4-colouring, that is, a mapping $c:V(G)\to \{0,1,2,3\}$ such that $c(u)\not =c(v)$ for every edge of $G$ with ends $u$ and $v$. This was conjectured by F. Guthrie in 1852, and remained open until a proof was found by Appel and Haken \cite{3}, \cite{4}, \cite{5} in 1976. Unfortunately, the proof by Appel and Haken (briefly, A\&H) has not been fully accepted. There has remained a certain amount of doubt about its validity, basically for two reasons: \begin{enumerate} \renewcommand{\theenumi}{\roman{enumi}} \renewcommand{\labelenumi}{(\theenumi)} %\list {(i)} \item %{ part of the A\&H proof uses a computer, and cannot be verified by hand, and %} %\list {(ii)} \item %{ even the part of the proof that is supposed to be checked by hand is extraordinarily complicated and tedious, and as far as we know, no one has made a complete independent check of it. %} \end{enumerate} Reason (i) may be a necessary evil, but reason (ii) is more disturbing, particularly since the 4CT has a history of incorrect ``proofs''. So in 1993, mainly for our own peace of mind, we resolved to convince ourselves somehow that the 4CT really was true. We began by trying to read the A\&H proof, but very soon gave this up. To check that the members of their ``unavoidable set'' were all reducible would require a considerable amount of programming, and {\em also} would require us to input by hand into the computer descriptions of $1478$ graphs; and this was not even the part of their proof that was most controversial. We decided it would be easier, and more fun, to make up our own proof, using the same general approach as A\&H. So we did; it was a year's work, but we were able to convince ourselves that the 4CT is true and provable by this approach \cite{14}. In addition, our proof turned out to be simpler than that of A\&H in several respects. The basic idea of the proof is the same as that of A\&H. We exhibit a set of ``configurations''; in our case there are 633 of them. We prove that none of these configurations can appear in a minimal counterexample to the 4CT, because if one appeared, it could be replaced by something smaller, to make a smaller counterexample to the 4CT (this is called proving ``reducibility''; here we are doing exactly what A\&H and several other authors did --- for instance, \cite{1}, \cite{2}, \cite{5}, \cite{9}). But every minimal counterexample is an ``internally 6-connected triangulation'' (defined later), and in the second part of the proof we prove that at least one of the 633 configurations appears in {\em every} internally 6-connected triangulation. (This is called proving ``unavoidability''.) Consequently, there is no minimal counterexample, and so the 4CT is true. Where our method differs from A\&H is in how we prove unavoidability. Some aspects of this difference are: we confirm Heesch's conjecture that one can prove unavoidability of some reducible set without looking beyond the second neighbourhoods of ``overcharged'' vertices; consequently, we avoid the problems with configurations that ``wrap around and meet themselves'', that were a major source of complications for A\&H; our unavoidable set has size about half that of the A\&H set; our ``discharging procedure'' for proving unavoidability (derived from an elegant method of Mayer \cite{13}) only involves 32 discharging rules, instead of the 487 of A\&H; and we obtain a quadratic time algorithm to find a 4-colouring of a planar graph, instead of the quartic algorithm of A\&H. Our proof is also somewhat easier to check, because we replace the mammoth hand-checking of unavoidability that A\&H required, by another mammoth hand-checkable proof, but this time written formally so that, if desired, it can be read and checked by a computer in a few minutes. We are making the necessary programs and data available to the public for checking via ``anonymous ftp'' from ftp.math.gatech.edu in the directory pub/users/thomas/four. The paper is organized as follows. In section 2 we introduce the concept of a configuration, and state the two main results. In section 3 we discuss reducibility, and in section 4 unavoidability. In section 5 we briefly discuss a quadratic algorithm to $4$--colour planar graphs, and in section 6 we make some concluding remarks. \section*{2. Configurations } The {\em degree} of a vertex $v$ of a graph $G$ is the number of edges incident with it, and is denoted by $d_{G}(v)$. A region of a plane graph is a {\em triangle} if it is incident with precisely three edges. A plane graph is a {\em triangulation} if it is connected, loopless and every region is a triangle. Thus, a triangulation can have parallel edges, but no circuit of length two bounds a region. A {\em minimal counterexample} means a plane graph $G$ that is not 4-colourable, such that every plane graph $G'$ with $|V(G')|+|E(G')|<|V(G)|+|E(G)|$ is 4-colourable. To prove the 4CT we must show that there is no minimal counterexample. It is easy to show that every minimal counterexample is a triangulation, and almost is 6-connected. More precisely, let us say a graph $G$ is {\em internally $6$-connected} if $G$ has at least six vertices, and for every set $X$ of vertices of $G$ such that the graph $G\backslash X$ obtained from $G$ by deleting $X$ is disconnected, either $|X|\ge 6$, or $|X|=5$ and $G\backslash X$ has exactly two components, one of which has exactly one vertex. Thus every vertex of an internally $6$-connected graph has degree at least five. We have (see, for example, \cite{7}) \begin{theorem1} Every minimal counterexample is an internally 6-connected triangulation. \end{theorem1} A {\em near-triangulation} is a non-null connected loopless plane graph $G$ such that every finite region is a triangle. A {\em configuration} $K$ consists of a near-triangulation $G(K)$ and a map $\gamma _{K}\colon V(G(K))\to \mathbb {Z}$ with the following properties: \begin{enumerate} \renewcommand{\theenumi}{\roman{enumi}} \renewcommand{\labelenumi}{(\theenumi)} %\list {(i)} \item %{ for every vertex $v$, $G(K)\backslash v$ has at most two components, and if there are two, then $\gamma _{K}(v)=d(v)+2$, %} %\list {(ii)} \item %{ for every vertex $v$, if $v$ is not incident with the infinite region, then $\gamma _{K}(v)=d(v)$, and otherwise $\gamma _{K}(v)>d(v)$; and in either case $\gamma _{K}(v)\ge 5$, %} %\list {(iii)} \item %{ $K$ has ring-size $\ge 2$, where the {\em ring-size} of $K$ is defined to be $\sum \limits _{v}(\gamma _{K}(v)-d(v)-1)$, summed over all vertices $v$ incident with the infinite region such that $G(K)\backslash v$ is connected. %} \end{enumerate} Two configurations are {\em isomorphic} if there is a homeomorphism of the plane mapping $G(K)$ to $G(L)$ and $\gamma _{K}$ to $\gamma _{L}$. In \cite{14} we exhibit a set of $633$ configurations that are essential to our proof. The set is also available in electronic form by ``anonymous ftp" as described earlier. Due to space limitations the full set cannot be described here, but in Figure 1 we show a small subset that will be referred to later in the paper. In Figure 1 we use a convention introduced by Heesch \cite{11}. The shapes of vertices indicate the value of $\gamma _{K}(v)$ as follows: A solid black circle means $\gamma _{K}(v)=5$, a dot (or what appears in the picture as no symbol at all) means $\gamma _{K}(v)=6$, a hollow circle means $\gamma _{K}(v)=7$, and a hollow square means $\gamma _{K}(v)=8$. (We will not need vertices $v$ with $\gamma _{K}(v)>8$ in this paper.) \begin{figure}[t] \includegraphics{era3e-fig-1} \caption{A set of configurations.} \end{figure} Any configuration isomorphic to one of the $633$ configurations exhibited in \cite{14} is called a {\em good} configuration. Let $T$ be a triangulation. A configuration $K$ {\em appears} in $T$ if $G(K)$ is an induced subgraph of $T$, every finite region of $G(K)$ is a region of $T$, and $\gamma _{K}(v)=d_{T}(v)$ for every vertex $v\in V(G(K))$. We prove the following two statements. \begin{theorem2} If $T$ is a minimal counterexample, then no good configuration appears in $T$. \end{theorem2} \begin{theorem3} For every internally $6$-connected triangulation $T$, some good configuration appears in $T$. \end{theorem3} From (2.1), (2.2) and (2.3) it follows that no minimal counterexample exists, and so the 4CT is true. We shall discuss (2.2) in section 3, and (2.3) in section 4. The first proof needs a computer. The second can be checked by hand in a few months, or, using a computer, it can be verified in a few minutes. \section*{3. Reducibility } By a {\em circuit} we mean a non-null connected graph in which every vertex has degree two. Let $K$ be a configuration. A near-triangulation $S$ is a {\em free completion of $K$ with ring} $R$ if \begin{enumerate} \renewcommand{\theenumi}{\roman{enumi}} \renewcommand{\labelenumi}{(\theenumi)} %\list {(i)} \item %{ $R$ is an induced circuit of $S$, and bounds the infinite region of $S$, %} %\list {(ii)} \item %{ $G(K)$ is an induced subgraph of $S$, $G(K)=S \backslash V(R)$, every finite region of $G(K)$ is a finite region of $S$, and the infinite region of $G(K)$ includes $R$ and the infinite region of $S$, and %} %\list {(iii)} \item %{ every vertex $v$ of $S$ not in $V(R)$ has degree $\gamma _{K}(v)$ in $S$. %} \end{enumerate} It is easy to check that every configuration has a free completion. (This is where we use the condition that ring-size $\ge 2$ in the definition of a configuration --- the ring-size is actually the length of the ring in the free completion, as the reader may verify.) Moreover, if $S_{1}$, $S_{2}$ are two free completions of $K$, there is a homeomorphism of the plane fixing $G(K)$ pointwise and mapping $S_{1}$ to $S_{2}$. (This is where condition (i) in the definition of a configuration is used.) Thus, there is essentially only one free completion, and so we may speak of ``the'' free completion without serious ambiguity. Let $R$ be a circuit. There is a concept of ``consistency" of a set of $4$-colourings of $R$ which essentially dates back to Kempe \cite{12} and Birkhoff \cite{7}. We will not define this concept here, but instead mention the properties we need. They are: \begin{enumerate} \renewcommand{\theenumi}{\roman{enumi}} \renewcommand{\labelenumi}{(\theenumi)} %\list {(i)} \item %{ the empty set is consistent, %} %\list {(ii)} \item %{ the union of any two consistent sets is consistent, %} %\list {(iii)} \item %{ if $T$ is a triangulation, $R$ is a circuit of $T$, $T'$ is the near-triangulation obtained from $T$ by deleting all vertices of $T$ that belong to the open disc bounded by $R$, and ${\mathcal{C}}$ is the set of restrictions of all $4$-colourings of $T'$ to $R$, then ${\mathcal{C}}$ is consistent, and %} %\list {(iv)} \item %{ consistency is sufficiently restrictive to permit enough reducible configurations (defined later). %} \end{enumerate} Let $S$ be the free completion of a configuration $K$ with ring $R$. Let ${\mathcal{C}}^{\ast }$ be the set of all $4$-colourings of $R$, and let ${\mathcal{C}}$ be the set of all restrictions to $V(R)$ of $4$-colourings of $S$. Let ${\mathcal{C}}'$ be the maximal consistent subset of ${\mathcal{C}}^{\ast }-{\mathcal{C}}$. (This is well defined by (i) and (ii).) The configuration $K$ is said to be $D$-{\em reducible} if ${\mathcal{C}}' =\emptyset $, and is said to be $C$-{\em reducible} if there exists a near-triangulation $S'$, called a {\em reducer}, obtained from $S$ by replacing $G(K)$ by a smaller graph (and possibly identifying some vertices of $R$) such that no member of ${\mathcal{C}}'$ is the restriction to $V(R)$ of a $4$-colouring of $S'$. It is reasonably easy to show that no $D$-reducible configuration can appear in a minimal counterexample. (Notice that the appearance of a configuration in $T$ does not imply that the free completion is a subgraph of $T$, but this difficulty is easy to take care of.) A more serious problem arises with $C$-reduction. There the natural proof that no $C$-reducible configuration can appear in a minimal counterexample would ``replace" $S$ by $S'$ in $T$, but how do we know that the resulting graph is loopless? Let us call a reducer {\em safe} if the above process results in a triangulation for every internally $6$-connected triangulation $T$. Checking safety was a major source of complications for A\&H, and one advantage of our new proof is that we are able to avoid these difficulties. The way we handle this problem is that we only consider reducers that are obtained from $K$ by contracting at most four edges, for which the safety check is easy. In order to prove (2.2) we show that \begin{theorem4} Each of the good $633$ configurations is either $D$-reducible or $C$-reducible with a safe reducer. \end{theorem4} Theorem (3.1) is proved by means of a computer program that is available to the public for examination. In fact, we used two independent programs that also computed some numerical invariants that could be compared to double-check our results. \section*{4. Unavoidability } A configuration $K$ {\em appears} in a configuration $L$ if $G(K)$ is an induced subgraph of $G(L)$, every finite region of $K$ is a finite region of $L$ (and hence the infinite region of $K$ includes the infinite region of $L$), and $\gamma _{K}(v)=\gamma _{L} (v)$ for every $v\in V(G(K))$. Let $T$ be an internally $6$-connected triangulation. For a vertex $v$ of $T$ we define the {\em vicinity} of $v$ in $T$ to be the configuration $K$ with $G(K)$ the subgraph of $T$ induced by all vertices $u$ of $T$ such that there is a path $P$ in $T$ with ends $u$ and $v$ with at most three vertices, and such that the interior vertex of $P$ (if there is one) has degree at most eight, and $\gamma _{K}(v)=d_{T}(v)$ for $v\in V(G(K))$. To prove (2.3) we show that a good configuration appears in the vicinity of some vertex. We now explain how we locate such a vertex. A {\em rule} is a $6$-tuple $(G,\alpha ,\epsilon ,r,s,t)$, where $G$ is a near-triangulation, $\alpha $ and $\epsilon $ are mappings from $V(G)$ to $\{5,6,7,8\}$ and $\{-,0,+\}$, respectively, $r>0$ is an integer, and $s$ and $t$ are distinct adjacent vertices of $G$. Figure 2 describes a set ${\mathcal{R}}$ of $32$ rules as follows. The mapping $\alpha $ is described using the same conventions as for Figure 1, $\epsilon $ is described by placing an appropriate sign next to the corresponding vertex (``0" is omitted), $r=2$ for the first rule and $r=1$ for all the other rules, and $s,t\in V(G)$ are such that the unique directed edge of the rule is directed from $s$ to $t$. There is some system in the first nine rules, but the other rules were chosen by trial and error, and have no particular plan or pattern. \begin{figure}[t] %\vskip 4in \includegraphics{era3e-fig-2} \caption{The set ${\mathcal{R}}$ of rules.} \end{figure} A {\em pass} $P$ is a quadruple $(K,r,s,t)$, where $K$ is a configuration, $r>0$ is an integer and $s,t\in V(G(K))$ such that there exists a rule $R=(G,\alpha ,\epsilon ,r,s',t')\in {\mathcal{R}}$ and a homeomorphism $h$ of the plane mapping $G(K)$ onto $G$ such that \begin{enumerate} \renewcommand{\theenumi}{\roman{enumi}} \renewcommand{\labelenumi}{(\theenumi)} %\list {(i)} \item %{ $\gamma _{K}(v)\le \alpha (h(v))$ for every $v\in V(G(K))$ with $\epsilon (h(v))\in \{-,0\}$, %} %\list {(ii)} \item %{ $\gamma _{K}(v)\ge \alpha (h(v))$ for every $v\in V(G(K))$ with $\epsilon (h(v))\in \{0,+\}$, and %} %\list {(iii)} \item %{ $h(s)=s'$ and $h(t)=t'$. %} \end{enumerate} We say that $P$ {\em obeys} rule $R$. It is straightforward to verify that every pass obeys exactly one rule. We write $r(P)=r$, $s(P)=s$, $t(P)=t$, and $K(P)=K$. We call $r$ the {\em value} of the pass, $s$ its {\em source}, and $t$ its {\em sink}. A pass $P$ {\em appears} in a triangulation $T$ if $K (P)$ appears in $T$. A pass $P$ {\em appears} in a configuration $L$ if $K(P)$ appears in $L$. If $v$ is a vertex of a triangulation $T$, we define $\Theta _{T}(v)$ to be \begin{equation*}\begin{split}10(6-d_{T}(v)) &+ \sum (r(P)\colon P~\hbox {appears~in~}T\,,~t(P)=v)\\ &-\sum (r(P)\colon P~\hbox {appears~in}~T\,,~s(P) =v)\,.\end{split}\end{equation*} We remark that $\Theta _{T}(v)$ depends only on the vicinity of $v$ in $T$. It follows from Euler's formula that \begin{theorem5} For every triangulation $T$, $\sum _{v\in V(T)} \Theta _{T}(v) =120$. In particular, there is a vertex $v$ of $T$ with $\Theta _{T}(v)>0$. \end{theorem5} Thus in order to prove (2.3) it suffices to prove \begin{theorem6} If $v$ is a vertex of an internally $6$-connected triangulation $T$ with $\Theta _{T}(v)>0$, then a good configuration appears in the vicinity of $v$ in $T$. \end{theorem6} Let $C_{1},C_{2},\ldots ,C_{17}$ be the configurations pictured in Figure 1. The following can be shown without the use of a computer. \begin{theorem7} If $v$ is a vertex of an internally $6$-connected triangulation $T$ with $\Theta _{T}(v)>0$, and either $d_{T}(v)\ge 12$ or $d_{T}(v)\le 6$, then a configuration isomorphic to one of $C_{1},C_{2},\ldots ,C_{17}$ appears in the vicinity of $v$ in $T$. \end{theorem7} \begin{proof}[Sketch of proof] Assume that $d_{T}(v)\ge 12$, and suppose that no such configuration appears. Let $d_{T}(v) = d$ and let $D$ be the set of neighbours of $v$. For each $u \in D$, let $R(u)$ be the sum of $r(P)$ over all passes $P$ appearing in $T$ with source $u$ and sink $v$. It can be shown that $R(u)\le 5$ for every $u\in D$ (we omit the details --- this is just a finite case analysis). Thus $\sum _{u\in D}R(u) \le 5d $, and hence \begin{equation*}\Theta _{T}(v) = 10 (6-d) + \sum _{u\in D}R(u) \le 10(6-d) + 5d = 60-5d \le 0\,,\end{equation*} a contradiction. This completes the proof in the case when $d_{T}(v)\ge 12$. We omit the other part, because, again, it is just a finite case analysis. \end{proof} Thus in order to prove (4.2) and hence (2.3) it remains to prove the following. \begin{theorem8} If $v$ is a vertex of an internally $6$-connected triangulation $T$ with $\Theta _{T}(v)>0$ and $d_{T}(v)=7,8,9,10$ or $11$, then a good configuration appears in the vicinity of $v$ in $T$. \end{theorem8} For each of the five cases, we have a proof. Unfortunately they are very long (altogether about 13,000 lines, and a large proportion of the lines take some thought to verify), and so cannot be included in a journal article. Moreover, although any line of the proofs can be checked by hand, the proofs themselves are not ``really'' checkable by hand because of their length. We therefore wrote the proofs so that they are machine-readable, and in fact a computer can check these proofs in a few minutes. More information is given in \cite[Section 7]{14}, and full details can be obtained by ``anonymous ftp" as described earlier. Alternatively, one can write a computer program to check (4.4) directly, for it is easily seen to be a finite problem. \section*{5. An algorithm} Our proof gives a quadratic algorithm to four-colour planar graphs, which is an improvement over the quartic algorithm of A\&H. Let us clarify a possible confusion here. It might appear that there is an ``obvious" quadratic algorithm as follows. Given an input plane graph $G$ on $n$ vertices (which may as well be assumed to be a triangulation) we find a good configuration appearing in $G$, replace $G$ by a smaller graph $G'$, and apply recursion. A reducible configuration can be found in linear time, and a $4$-colouring of $G$ can be constructed from a $4$-colouring of $G'$ in linear time. Since there are at most $n$ recursive steps, the overall running time would be quadratic. The problem is that (2.3) only guarantees the appearance of a good configuration if $G$ is an internally $6$-connected triangulation, and yet even if we started with a highly connected graph, the connectivity is bound to drop during the recursion. However, (4.2) permits us to quickly find either a good configuration appearing in $G$, in which case we proceed as suggested above, or a set $X$ of vertices of $G$ violating the definition of internal $6$-connection, in which case we apply recursion to two carefully selected subgraphs of $G$, and then obtain a $4$-colouring of $G$ by piecing together $4$-colourings of the two subgraphs. We refer to \cite{14} for further details. \section*{6. Discussion} This concludes our discussion of the proof of the 4CT and the associated algorithm. A full account can be found in \cite{14} except for the proofs of (3.1) and (4.4). Those two theorems are just stated in \cite{14} as having been proved by a computer. Verifying (3.1) takes about 3 hours on a Sun Sparc 20 workstation, and (4.4) takes about 20 minutes altogether. Both need less than one megabyte of RAM. The complete programs as well as documenation for them \cite{15}, \cite{16} can be obtained for examination by ``anonymous ftp" as described earlier. Thus we are making it possible for other scientists to verify all steps in our proof, including the computer programs and data. We should mention that both our programs use only integer arithmetic, and so we need not be concerned with round-off errors and similar dangers of floating point arithmetic. However, an argument can be made that our ``proof" is not a proof in the traditional sense, because it contains steps that can never be verified by humans. In particular, we have not proved the correctness of the compiler we compiled our programs on, nor have we proved the infallibility of the hardware we ran our programs on. These have to be taken on faith, and are conceivably a source of error. However, from a practical point of view, the chance of a computer error that appears consistently in exactly the same way on all runs of our programs on all the compilers under all the operating systems that our programs run on is infinitesimally small compared to the chance of a human error during the same amount of case-checking. Apart from this hypothetical possibility of a computer consistently giving an incorrect answer, the rest of our proof can be verified in the same way as traditional mathematical proofs. We concede, however, that verifying a computer program is much more difficult than checking a mathematical proof of the same length. \bibliographystyle{amsplain} \begin{thebibliography}{99} \bibitem{1} F. Allaire, {\em Another proof of the four colour theorem-{\rm Part I}}, Proc. of the 7th Manitoba Conf. on Numerical Math. and Computing (1977), Congressus Numerantium XX, Utilitas Math., Winnipeg, 1978, pp.~3--72. \MR{80m:05031} \bibitem{2} F. Allaire and E. R. Swart, {\em A systematic approach to the determination of reducible configurations in the four-color conjecture}, J. Combinatorial Theory, Ser. B {\bf 25} (1978), 339--362. \MR{80i:05041} \bibitem{3} K. Appel and W. Haken, {\em Every planar map is four colorable. Part I. Discharging}, Illinois J. Math. {\bf 21} (1977), 429--490. \MR{58:27598d} \bibitem{4} K. Appel, W. Haken, and J. Koch, {\em Every planar map is four colorable. Part II. Reducibility}, Illinois J. Math {\bf 21} (1977), 491--567. \MR{58:27598d} \bibitem{5} K. Appel and W. Haken, {\em Every planar map is four colorable}, A.M.S. Contemporary Math. {\bf 98} (1989). \MR{91m:05079} \bibitem{6} A. Bernhart, {\em Another reducible edge configuration}, Amer. J. Math. {\bf 70} (1948), 144--146. \MR{9:366g} \bibitem{7} G. D. Birkhoff, {\em The reducibility of maps}, Amer. J. Math. {\bf 35} (1913), 114--128. \bibitem{8} D. I. A. Cohen, {\em Block count consistency and the four color problem}, manuscript. \bibitem{9} K. D\"{u}rre, H. Heesch, and F. Miehe, {\em Eine Figurenliste zur chromatischen Reduktion}, manuscript eingereicht am 15.8.1977. \bibitem{10} S. J. Gismondi and E. R. Swart, {\em A new type of 4-colour reducibility}, Congr. Numer. {\bf 82} (1991), 33--48. \MR{92j:05069} \bibitem{11} H. Heesch, {\em Untersuchungen zum Vierfarbenproblem}, Hochschulskriptum 810/a/b, Bibliographisches Instit\"{u}t, Mannheim, 1969. \MR{40:1303} \bibitem{12} A. B. Kempe, {\em On the geographical problem of the four colors}, Amer. J. Math. {\bf 2} (1879), 193--200. \bibitem{13} J. Mayer, {\em Une propri\'{e}t\'{e} des graphes minimaux dans le probl\`{e}me des quatre cou\-leurs}, Probl\`{e}mes Combinatoires et Th\'{e}orie des Graphes, Colloques internationaux CNRS No. 260, Paris, 1978. \MR{80m:05042} \bibitem{14} N. Robertson, D. P. Sanders, P. D. Seymour, and R. Thomas, {\em The four colour theorem}, manuscript. \bibitem{15} \bysame, {\em Reducibility in the four colour theorem}, unpublished manuscript available from \newline ftp://ftp.math.gatech.edu/pub/users/thomas/four. \bibitem{16} \bysame, {\em Discharging cart\-wheels}, unpublished manuscript available from \newline ftp://ftp.math.gatech.edu/pub/users/thomas/four. \bibitem{17} P. G. Tait, {\em Note on a theorem in geometry of position}, Trans. Roy. Soc. Edinburgh {\bf 29} (1880), 657--660. \bibitem{18} H. Whitney and W. T. Tutte, {\em Kempe chains and the four colour problem}, Studies in Graph Theory (D. R. Fulkerson, eds.), Part II, Math. Assoc. of America, 1975, pp.~378--413. \MR{52:13468} \end{thebibliography} \end{document}