Four color theorem
|
|
FourColorMapEx.png
The four color theorem states that any plane separated into regions, such as a political map of the counties of a state, can be colored using no more than four colors in such a way that no two adjacent regions receive the same color. Two regions are called adjacent if they share a border segment, not just a point. Each region must be contiguous - that is it may not be partitioned as are Michigan and Azerbaijan.
It is obvious that three colors are inadequate, and it is not at all difficult to prove that five colors are sufficient to color a map.
The four color theorem was the first major theorem to be proven using a computer, and the proof is not accepted by all mathematicians because it would be infeasible for a human to verify by hand. Ultimately, one has to have faith in the correctness of the compiler and hardware executing the program used for the proof.
The lack of mathematical elegance was another factor, and to paraphrase comments of the time, "a good mathematical proof is like a poem — this is a telephone directory!"
| Contents |
History
The conjecture was first proposed in 1852 when Francis Guthrie, while trying to color the map of counties of England, noticed that only four different colors were needed. At the time, Guthrie was a student of Augustus De Morgan at University College. (Guthrie graduated in 1850, and later became a professor of mathematics in South Africa). According to de Morgan:
- A student of mine [Guthrie] asked me today to give him a reason for a fact which I did not know was a fact - and do not yet. He says that if a figure be anyhow divided and the compartments differently coloured so that figures with any portion of common boundary line are differently coloured - four colours may be wanted, but not more - the following is the case in which four colours are wanted. Query cannot a necessity for five or more be invented...
The first published reference is found in Arthur Cayley's, On the colourings of maps., Proc. Royal Geography Society 1, 259-261, 1879.
There were several early failed attempts at proving the theorem. One proof of the theorem was given by Alfred Kempe in 1879, which was widely acclaimed; another proof was given by Peter Tait in 1880. It wasn't until 1890 that Kempe's proof was shown incorrect by Percy Heawood, and 1891 that Tait's proof was shown incorrect by Julius Petersen - each false proof stood unchallenged for 11 years.
In 1890, in addition to exposing the flaw in Kempe's proof, Heawood proved that all planar graphs are five-colorable; see five color theorem.
Significant results were produced by Croatian mathematician Danilo Blanuša in the 1940s by finding an original snark.
During the 1960s and 70s German mathematician Heinrich Heesch developed methods of applying the computer in searching for a proof.
In 1969 British mathematician G. Spencer-Brown claimed that the theorem could be proven with mathematics he had developed. However, he was never able to produce a proof.
It was not until 1976 that the four-color conjecture was finally proven by Kenneth Appel and Wolfgang Haken at the University of Illinois. They were assisted in some algorithmic work by J. Koch.
The proof reduced the infinitude of possible maps to 1,936 configurations (later reduced to only 1,476) which had to be checked one by one by computer. The work was independently double checked with different programs and computers. However, the proof was over 500 pages of hand written counter-counter-examples, much of which was Haken's teenage son verifying graph colorings. The computer program ran for hundreds of hours.
In 1996, Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas produced a similar proof which required checking 633 special cases. This new proof also contains parts which require the use of a computer and are impractical for humans to check alone.
In 2004, Benjamin Werner and Georges Gonthier formalized a proof of the theorem inside the Coq theorem prover. This removes the need to trust the various computer programs used to verify particular cases — it is only sufficient to trust the Coq prover.
Since the proving of the theorem, efficient algorithms have been found for 4-coloring maps requiring only O(n2) time, where n is the number of vertices. There are also efficient algorithms to determine whether 1 or 2 colors are enough to color a map. Determining whether 3 colors suffices is, however, NP-complete, and so unlikely to have a fast solution. Determining whether a general (possibly non-planar) graph can be 4-colored is also NP-complete.
Not for map-makers
The four colour theorem does not arise out of and has no origin in practical cartography. According to Kenneth May, a mathematical historian who studied a sample of atlases in the Library of Congress, there is no tendency to minimise the number of colors used. Maps utilizing only four colors are rare, and those that do usually require only three.
Textbooks on cartography and the history of cartography don't mention the four colour theorem, even though map colouring is a subject of discussion. Generally, mapmakers say they are more concerned about coloring maps in a balanced fashion, so that no single color dominates. Whether they use 4 or 5 colors is not their primary concern.
Formal statement in graph theory
To formally state the theorem, it is easiest to rephrase it in graph theory. It then states that the vertices of every planar graph can be colored with at most four colors so that no two adjacent vertices receive the same color. Or "every planar graph is four-colorable" for short. Here, every region of the map is replaced by a vertex of the graph, and two vertices are connected by an edge if and only if the two regions share a border segment (not just a corner).
Generalizations
One can also consider the coloring problem on surfaces other than the plane. The problem on the sphere is equivalent to that on the plane. For closed (orientable or non-orientable) surfaces with positive genus, the maximum number p of colors needed depends on the surface's Euler characteristic χ according to the formula
- <math>p=\left\lfloor\frac{7 + \sqrt{49 - 24 \chi}}{2}\right\rfloor<math>,
where the outermost brackets denote the floor function. The only exception to the formula is the Klein bottle, which has Euler characteristic 0 and requires 6 colors. This was initially known as the Heawood conjecture and proved as The Map Color Theorem by Gerhard Ringel and J. T. W. Youngs in 1968.
For example, the torus has Euler characteristic χ = 0 and requires p = 7 colors. In a torus, you need 7 colors to paint any map.
Real world counterexamples
In the real world, not all countries are contiguous (e.g. Alaska as part of the United States). If the chosen coloring scheme requires that the territory of a particular country must be the same color, four colors may not be sufficient. Conceptually, a constraint such as this enables the map to become non-planar, and thus the four color theorem no longer applies. For instance, consider a simplified map:
In this map, the two regions labeled A belong to the same country, and must be the same color. This map then requires five colors, since the two A regions together are contiguous with four other regions, each of which is contiguous with all the others. If A consisted of three regions, six or more colors might be required; one can construct maps that require an arbitrarily high number of colors.
Theorem proved: four colors suffice
After many faulty attempts the theorem was proved by Kenneth Appel and Wolfgang Haken, publicly announced 22 July 1976, and published in 1977.
The proof of the Four Color Theorem is not simple; it involved more than 1,000 hours of computing time on a 1977 computer checking more than 100,000 particular cases. To some mathematicians this is unacceptable, as the proof cannot be reviewed; but would a 1,000-page hand-written proof be any more checkable?
What the proof does not provide is any insight as to why the conjecture is true. The theorem is true, but unexplained. This is another, stronger reason that critics call the proof inelegant.
In 2004, Benjamin Werner and Georges Gonthier from INRIA formalized a proof of the theorem inside the Coq theorem prover. This removes the need to trust the various computer programs used to verify particular cases — it is only sufficient to trust the Coq prover.
See also
References
- Appel, Kenneth & Haken, Wolfgang & Koch, John, Every Planar map is Four Colorable, Illinois: Journal of Mathematics: vol.21: pp.439-567, December 1977.
- Appel, Kenneth & Haken, Wolfgang, Solution of the Four Color Map Problem, Scientific American, vol.237 no.4: pp.108-121, October 1977.
- Appel, Kenneth & Haken, Wolfgang, Every Planar Map is Four-Colorable. Providence, RI: American Mathematical Society, 1989.
- O'Connor and Robertson, History of the Four Color Theorem, MacTutor project, http://www-groups.dcs.st-and.ac.uk/~history/HistTopics/The_four_colour_theorem.html
- Saaty and Kainen, The Four Color Problem: Assaults and Conquest (ISBN 0-486-65092-8)
- Robin Thomas, An Update on the Four-Color Theorem (http://www.ams.org/notices/199807/thomas.pdf) (PDF File), Notices of the American Mathematical Society, Volume 45, number 7 (August 1998)
- Robin Thomas, The Four Color Theorem, http://www.math.gatech.edu/~thomas/FC/fourcolor.htmlcs:Problém čtyř barev
de:Vier-Farben-Satz es:Teorema de los cuatro colores he:בעיית ארבעת הצבעים it:Teorema dei quattro colori nl:vierkleurenstelling ja:四色定理 pl:Twierdzenie o czterech kolorach pt:teorema das quatro cores fi:Nelivriongelma sv:Fyrfrgssatsen th:ทฤษฎีบทสี่สี zh:四色问题