Outdated Archival Version

These pages are not updated anymore. They reflect the state of 20 August 2005. 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}