An equivalent combinatorial interpretation is
This theorem was proved with the aid of a computer in 1976. The proof shows that if aprox. 1,936 basic forms of maps can be coloured with four colours, then any given map can be coloured with four colours. A computer program coloured these basic forms. So far nobody has been able to prove it without using a computer. In principle it is possible to emulate the computer proof by hand computations.
The known proofs work by way of contradiction. The basic thrust of the proof is to assume that there are counterexamples, thus there must be minimal counterexamples in the sense that any subset of the graphic is four colourable. Then it is shown that all such minimal counterexamples must contain a subgraph from a set basic configurations.
But it turns out that any one of those basic counterexamples can be replaced by something smaller, while preserving the need for five colours, thus contradicting minimality.
The number of basic forms, or configurations has been reduced to 633.
A recent simplification of the Four Colour Theorem proof, by Robertson, Sanders, Seymour and Thomas, has removed the cloud of doubt hanging over the complex original proof of Appel and Haken.
The programs can now be obtained by ftp and easily checked over for correctness. Also the paper part of the proof is easier to verify. This new proof, if correct, should dispel all reasonable criticisms of the validity of the proof of this theorem.
References
K. Appel and W. Haken. Every planar map is four colorable. Bulletin of the American Mathematical Society, vol. 82, 1976 pp.711-712.
K. Appel and W. Haken. Every planar map is four colorable. Illinois Journal of Mathematics, vol. 21, 1977, pp. 429-567.
N. Robertson, D. Sanders, P. Seymour, R. Thomas The Four Colour Theorem Preprint, February 1994. Available by anonymous ftp from ftp.math.gatech.edu, in directory /pub/users/thomas/fcdir/npfc.ps.
The Four Color Theorem: Assault and Conquest T. Saaty and Paul Kainen. McGraw-Hill, 1977. Reprinted by Dover Publications 1986.