Four color theorem

The four- color theorem (also four-color theorem, formerly known as the four-color conjecture or four-color problem) is a mathematical theorem and states that four colors always suffice any map in the Euclidean plane so colorize that no two adjacent countries get the same color. The rate shall be applied in the graph theory, topology and cartography.

This is subject to the restrictions that isolated common points do not count as " limit" and each country consists of a contiguous area, so no enclaves are present.

History

The phrase was first erected in 1852 by Francis Guthrie as conjecture, as he wanted to color the counties of England on a map. It was obvious that three colors are not sufficient - see right - and it took five in no contrived example. In a letter of the London Mathematics Professor Augustus De Morgan 23 October 1852 the Irish colleague William Rowan Hamilton, the conjecture was first discussed and published: " Suffice four or fewer colors to color the countries of a map so that adjacent countries have different colors wear? ".

The English mathematician Arthur Cayley introduced the issue in 1878 of the Mathematical Society of London. Within just one year, Alfred Kempe was an apparent proof of the theorem. Eleven years later, in 1890, showed Percy Heawood that Kempe's proof attempt was flawed. A second faulty proof attempt, published in 1880 by Peter Guthrie Tait, was also eleven years can not be refuted. Not until 1891 that showed Julius Petersen, that Tait's approach was incorrect. Heawood was in 1890 with the refutation of Kempe's " four-color proof" additional evidence for the five -color set with what an upper limit for the coloring of planar graphs without error demonstrated for the first time. In Kempe's failed attempt already infected basic ideas that led to the later proof by Appel and Haken.

Heinrich Heesch developed in the 1960s and 1970s, a first draft of a computer proof.

This was improved in 1976 by Kenneth Appel and Wolfgang hook. The proof reduced the number of problematic cases from infinity to 1936 ( a later version even 1476 ), which were tested individually by a computer.

In 1996, Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas find a modified computer evidence, which reduced the cases to 633. Also, they had to be checked by computer.

2005 Georges Gonthier and Benjamin Werner have constructed a formal proof of the theorem in the proof assistant Coq. Thus it is no longer necessary to rely on computer programs to check the individual cases, but "only" the Coq system.

The four- color theorem was the first major mathematical problem that has been solved with the help of computers. Therefore, the evidence of some mathematicians was not recognized because it can not be understood directly by a human. Finally, you have to rely on the correctness of the compiler and the hardware. The lack of mathematical elegance of the proof has been criticized.

Faulty evidence to the contrary

... At least four of the ten regions recolor to make do with only four colors.

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

Frequently, the simplest " counter-examples " a region which touches all other regions. This forces to get along with four colors to fill in the remaining regions with only three colors. The counter-examples overlook the fact that by re-coloring of the inner region precisely this can be achieved, as they rush too much on the outer area.

This trick can be generalized; it is easy to construct maps on which it is impossible to get along with four colors when the colors of some regions were defined in advance. A superficial reviewer of counter-example is often not remember recolor these regions.

Other false evidence to the contrary violate the assumptions of the theorem, for example, by using regions, which consist of several separate areas, or by banning same-colored regions that touch at only one point.

Formalization

Formally, the simplest solution is described with the help of graph theory. One wonders whether the node of each planar graphs with up to four colors can be dyed so that no adjacent nodes have the same color. Or shorter: " Is every planar graph 4 -colorable? " Here, every country in the map is assigned to exactly one node; the nodes adjacent countries are interconnected.

Modifications and generalizations

• Map on a torus that requires seven colors

Animated torus same card

The four-color problem is a special case of the Heawood conjecture. The classic four-color problem affects maps that lie on a plane or spherical surface. The Heawood conjecture, the analogous 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 - much easier to prove than the four- color theorem and comes without computer assistance from. JW Ted Youngs and Gerhard Ringel was in 1968 the first Heawood conjecture for all other cases prove ( set of Ringel- Youngs ). The four- color theorem is therefore not verified by this proof, but must be treated separately.

If we expand the terms of reference of the four- color theorem of surfaces on the Euclidean space itself, then there is no limit on the number of colors. Instead of the " countries" appear three-dimensional fields on ( "body" ) to be different colors if they have a common interface. For each number can construct an example that requires a minimum of colors. Think of "long" congruent cubes ( "bar" ) adjacent to each other, which together form a rectangular square base. Then lie again to the first congruent cubes next to each other but perpendicular to the bottom so that all the lower square touch, all the top square. Now each of the bottom is connected to exactly one of the upper, so that both crosswise form a body together. Each of these bodies touched each other; So you need colors and was arbitrary.

Remark

• The Kuratowski minors

And the

If (as in reality often the case ) a country is distributed among several non- adjacent areas ( colonies exclaves, ...), then its graph is not necessarily planar, and there may be more than four colors for coloring are necessary. On planarity can be tested given graphs very quickly. By the theorem of Kuratowski there are certain subgraphs that prevent the planarity of graphs. These are just two basic forms, the so-called Kuratowski minors and, and beyond their subdivisions. By a clever choice of data structures can be found and find that there is not it by often considered one each node and each edge only constant these " subgraph ".

To find the smallest possible coloring in general graphs to determine in other words, the so-called chromatic number, is very complex (more precisely, an NP-complete task). According to the testimony of Tutte they would be solved if you have found a smallest group in the dual graph, so that a gruppenwertige flow (which is a " flow without beginning or end "), which nowhere assumes the zero element exists. This group is called order flow number and it is for arbitrary graphs. The solvability of this remains NP- complete problem is independent of the structure of the given group and depends only on the group order.

There are other relationships of the four-color problem with problems of discrete mathematics, so you can also use methods of algebraic topology.