Four color set

Example of a four-coloration

The four-color theorem (also four-color theorem , formerly also known as the four-color conjecture or four-color problem ) is a mathematical theorem and states that four colors are always sufficient for any map in the Euclidean plane to be colored so that no two neighboring countries get the same color. The theorem is used in graph theory , topology and cartography .

This applies under the restrictions that isolated common points do not count as “borders” and that each country consists of a contiguous area, so there are no exclaves .

history

This card requires four different colors

The sentence was first put up as a guess by Francis Guthrie in 1852 when he wanted to color the counties of England on a map. It was obvious that three colors were not enough and five would not be needed in any constructed example. In a letter from London math professor Augustus De Morgan dated October 23, 1852 to his Irish colleague William Rowan Hamilton , the conjecture was first discussed and published: “Are four or fewer colors enough to color the countries on a map so that neighboring countries have different colors wear?"

The English mathematician Arthur Cayley introduced the problem to the Mathematical Society of London in 1878. Within just a year, Alfred Kempe found apparent evidence for the theorem. Eleven years later, in 1890, Percy Heawood showed that Kempe's attempt to prove it was flawed. A second erroneous attempt at proof, published by Peter Guthrie Tait in 1880 , could not be refuted for eleven years either. It was not until 1891 that Julius Petersen showed that Tait's approach was also incorrect. With the refutation of Kempe's “four-color proof” in 1890, Heawood also gave a proof for the five-color theorem , with which an upper bound for the coloring of planar graphs was proven error-free for the first time. Kempe's faulty experiment already contained fundamental ideas that led to later proof by Appel and Haken.

Free stamp with additional inscription Four colors suffice , used by the Mathematics Department of the UIUC after computer evidence in 1976

Heinrich Heesch developed a first draft of a computer proof in the 1960s and 1970s, but this was not realized due to a lack of computing time. This was improved by Kenneth Appel and Wolfgang Haken at the University of Illinois in 1976. The evidence reduced the number of problematic cases from infinity to 1936 (a later version even 1476), which were individually checked by a computer. After criticism of this evidence, Appel and Haken published a detailed description in 1989 with a 400-page appendix on microfilm.

In 1996, Neil Robertson , Daniel Sanders , Paul Seymour, and Robin Thomas were able to find modified computer evidence that reduced the cases to 633. These also had to be checked by computer.

In 2005, Georges Gonthier and Benjamin Werner constructed a formal proof of the theorem in the proof assistant Coq .

criticism

The four-color theorem was the first major math problem solved with the help of computers . Therefore, the proof was not recognized by some mathematicians because it cannot be directly understood by a human and because one has to rely on the correctness of the compiler and the hardware . The lack of mathematical elegance of the proof has also been criticized. In 1989, the graph theorist Horst Sachs explicitly expressed the opinion that the final solution to the four-color problem is still pending . The criticism has persisted in recent times and has been confirmed by the British mathematician Ian Stewart .

Incorrect evidence to the contrary

• 

  This card has been colored with five colors and you have to ...

• 

  ... color at least four of the ten regions to make do with only four colors.

Like many open problems in mathematics, the four-color theorem has provoked a lot of flawed evidence and counter-evidence. Some withstood public scrutiny for decades until they were recognized as false. Many others, mostly developed by amateurs, have never been published.

The simplest "counterexamples" often contain a region that affects all other regions. In order to get by with four colors, this forces the remaining regions to be filled with only three colors. The counterexamples overlook the fact that this can be achieved by changing the color of the inner area, since they lean too much on the outer area.

This trick can be generalized; it is easy to construct maps on which it is impossible to get by with four colors if the colors of some regions are determined in advance. Often, a cursory checker of the counterexample will not think of recoloring these regions.

Other false counter-evidence violates the assumptions of the theorem, for example by using regions that consist of several separate areas or by forbidding regions of the same color that only touch at one point.

Formalization

Representation of the formulation in graph theory

In formal terms, the easiest way to describe the problem is with the help of graph theory. One asks whether the nodes of every planar graph can be colored with a maximum of four colors in such a way that no neighboring nodes have the same color. Or, in short: “Can every planar graph be 4-colored ?” Each country on the map is assigned exactly one node; the nodes of neighboring countries are connected to one another.

Modifications and generalizations

• Map on a torus that requires seven colors
• 

  Map shown with 7 colorations in the plane

• 

  Animated torus of the same map

The four-color problem is a special case of the Heawood conjecture . The classic four-color problem concerns maps that lie on a plane or spherical surface. The Heawood conjecture poses the same question for general surfaces, such as the Klein bottle (6 colors), the Möbius strip (6 colors), the projective plane (6 colors) and the torus (7 colors). Interestingly, the generalization - apart from the special case for planes or spherical surfaces - is much easier to prove than the four-color theorem and does not require a computer. J. W. Ted Youngs and Gerhard Ringel were able to prove the Heawood conjecture for all other cases for the first time in 1968 ( theorem of Ringel-Youngs ). The four-color theorem is therefore not verified by this proof, but has to be treated separately.

After joining in the graphic on the right, the two “bars” of the same color are connected and each form a (L or X-shaped) body. Since every body touches every other, you need as many colors as bars (here 8) for dyeing.

If one extends the task of the four-color set of surfaces to three-dimensional Euclidean space, then there is no upper limit for the number of colors. Instead of the “countries”, three-dimensional areas (“bodies”) appear, which should have different colors if they have a common interface. For every number  an example can be constructed ( Heinrich Tietze ) that requires at least colors. Imagine “long” congruent cuboids (“bars”) lying next to each other, which together form a cuboid with a square base. Thereupon there are again cuboids that are congruent to the first, but perpendicular to the lower cuboids, so that all the lower cuboids touch all the upper cuboids. Now each of the lower ones is connected to exactly one of the upper ones, so that both together form a body crosswise . Each of these bodies touches each other; So you need colors and you were free . ${\displaystyle n}$ ${\displaystyle n}$ ${\displaystyle n}$ ${\displaystyle n}$ ${\displaystyle n}$ ${\displaystyle n}$

comment

• The Kuratowski Minors
• 

  Of the ${\displaystyle K_{5}}$

• 

  and the ${\displaystyle K_{3,3}}$

If (as is often the case in reality) a country is distributed over several non-contiguous areas ( colonies , exclaves , ...), then the associated graph is not necessarily planar and more than four colors may be necessary for coloring. Given graphs can be tested very quickly for planarity. According to Kuratowski's theorem, there are certain subgraphs that prevent graphs from being planar. There are exactly two basic forms, the so-called Kuratowski minors and , and also their subdivisions. With a skilful choice of the data structures one can find these "subgraphs" or determine that they do not exist by only looking at every node and every edge constantly. ${\displaystyle K_{5}}$ ${\displaystyle K_{3,3}}$

Finding the smallest possible color in general graphs , in other words determining the so-called chromatic number , is a very complex task (more precisely: in its decision variant NP-complete ). According to Tutte , it would be solved if a smallest group was found in the dual graph , so that a group-valued flow (that is a “ flow without beginning and end”) that does not assume the zero element anywhere exists. This group order is called the flow number and it is for any graph . The solvability of this still NP-complete problem is independent of the structure of the given group and only depends on the group order. ${\displaystyle G}$ ${\displaystyle \chi (G)}$ ${\displaystyle G^{*}}$ ${\displaystyle \varphi (G^{*})}$ ${\displaystyle \varphi (G^{*})=\chi (G)}$

There are further connections between the four-color problem and problems in discrete mathematics , so that methods of algebraic topology can also be used.

Time complexity

Computing a 4-coloring is possible for planar graphs with nodes in time . In contrast, the decision as to whether three colors are sufficient is NP-complete. ${\displaystyle n}$ ${\displaystyle O(n^{2})}$

Others

Some well-known mathematicians tried their hand at the proof. Max Born reports that Hermann Minkowski (1864–1909) attempted to prove it over several weeks in an introductory lecture on topology (with the introductory words that this would be a good introduction to topology and that only third-rate mathematicians have attempted it so far ) until he finally gave up. Born remembers that there was a thunderstorm at the time and Minkowski half jokingly said that the sky was angry about his presumptuousness.

Even Ernst Witt tried in the 1930s as a student at the evidence and presented it to Richard Courant ; But his friend Heinrich Heesch found a mistake, which was the beginning of his own preoccupation with the problem.

Other mathematicians who dealt with the problem and achieved significant partial results were Øystein Ore (who increased the minimum number of areas that can be colored with four colors to 40) and Hassler Whitney (in his dissertation from 1932).

There are also algebraically equivalent formulations ( Howard Levi , Juri Wladimirowitsch Matijassewitsch , M. Mnuk, Noga Alon ).

literature

• Neil Robertson, Daniel P. Sanders, Paul Seymour, Robin Thomas: A new proof of the four-color theorem. In: Electronic Research Announcements of the American Mathematical Society . 2/1996. Pp. 17-25.
• Kenneth Appel, Wolfgang Haken: Every Planar Map is Four Colorable. In: Contemp. Math. Vol. 98, Amer. Math. Soc., Providence, RI, 1989.
• Georges Gonthier: A computer-checked proof of the Four Color Theorem (PDF; 607 kB). unpublished, on this Gonthier: Formal proof- the four color theorem , Notices AMS 2008 (PDF).
• Rudolf Fritsch , Gerda Fritsch: The four-color theorem: history, topological foundations and idea of ​​proof. BI-Wissenschaftsverlag, 2004, ISBN 3-411-15141-2 ( PDF ).
• Robin Thomas: An update on the four color theorem. Notices AMS 1998, issue 7 ( PDF ).
• Gerhard Ringel : The card coloring problem . In: Selecta Mathematica III (Ed. Konrad Jacobs) (=  Heidelberger Taschenbücher . Volume 86 ). Springer Verlag , Berlin, Heidelberg, New York 1971, ISBN 3-540-05333-6 ( MR0543809 ).
• Ian Stewart: The Final Riddles of Mathematics . 2nd Edition. Rowohlt Taschenbuch Verlag , Reinbek bei Hamburg 2015, ISBN 978-3-499-61694-5 .
• Lutz Volkmann : Foundations of the graph theory . Springer Verlag, Vienna, New York 1996, ISBN 3-211-82774-9 ( MR1392955 ).
• Robin Wilson Four colors suffice. Princeton University Press 2002, Review in the AMS Notices, 2004, PDF file

Web links

Commons : four-color set  - collection of images, videos and audio files

• Summary of the evidence by Robertson, Sanders, Seymour, Thomas on Robin Thomas' homepage
• Simon Tatham's Portable Puzzle Collection The Map game covers the theme.
• Reformulating the Map Color Theorem by Louis H. Kauffman (PDF; 589 kB). Reformulation of the four-color problem taking into account George Spencer-Brown's approach in Laws of Form

Footnotes

1. ↑ ^{a b} Robin Wilson [2002]: Four Colors Suffice  (= Princeton Science Library). Princeton University Press, Princeton, NJ 2014, ISBN 978-0-691-15822-8 .
2. ^ Gary Chartrand, Linda Lesniak: Graphs & Digraphs . CRC Press, 2005, p. 221.
3. ↑ Kenneth Appel, Wolfgang Haken (with the collaboration of J. Koch): Every Planar Map is Four-Colorable . In: Contemporary Mathematics . tape 98 . American Mathematical Society, Providence, RI 1989, ISBN 0-8218-5103-9 , doi : 10.1090 / conm / 098 .
4. ^ ^{A b} Neil Robertson, Daniel P. Sanders, Paul Seymour, Robin Thomas: Efficiently four-coloring planar graphs . In: ACM Press (Ed.): STOC'96: Proceedings of the twenty-eighth annual ACM symposium on Theory of computing . 1996, pp. 571-575. doi : 10.1145 / 237814.238005 .
5. ^ Georges Gonthier: Formal Proof — The Four-Color Theorem . In: Notices of the American Mathematical Society . 55, No. 11, 2008, pp. 1382-1393.
6. ^ Lutz Volkmann: Foundations of the graph theory. 1996, pp. 254-255.
7. ↑ Ian Stewart: The Final Riddles of Mathematics. 2015, pp. 131–136.
8. ↑ Christoph Joachim Scriba , Peter Schreiber: 5000 years of geometry. 2nd Edition. Springer, Berlin 2005, ISBN 3-540-22471-8 , p. 454 and Fig. 7.8.3
9. ↑ Further statements and sentences on this in Reinhard Diestel : Graph Theory. Springer, 2000, ISBN 0-387-98976-5 , p. 157 ff.
10. ↑ Michael R. Garey, David S. Johnson: Computers and Intractability - A Guide to the Theory of NP Completeness. WH Freeman, 1979. ISBN 0-7167-1045-5 , pp. 87ff.
11. ^ Born: Memories of Hermann Minkowski on the return of the 50th anniversary of his death. Die Naturwissenschaften, Volume 46, 1959, p. 501
12. ^ Melvin Fitting: The Four Color Theorem. Lehman College, CUNY