# Four-color set

the four-color set (in former times also as four-color assumption or four-color problem admits) of the graph theory, topology and/or. Cartography means that four colors are always sufficient, in order to dye any map in such a way that no two adjacent countries get the same color.

This applies underthe restrictions that a common point not when “border” counts and of a connected surface consists each country thus no Exklaven it is present.

Example of a four-colouring

## History

the sentence was set up to 1852 for the first time of Francis Guthrie as assumption, when it wanted to color the Counties of England. It was obvious that three colors were not sufficient and one needed five in no designed example. In a letter of theLondoner of mathematics professor Augustus De Morgan of 23. October 1852 at the Irish colleague William Rowan Hamilton was discussed for the first time and published the assumption: To color “being sufficient four or fewer colors around the countries of a map in such a way that neighbouring countries differentColors carry? “.

The English mathematician Arthur Cayley presented the problem of 1878 to the mathematical society of London. Within only a yearly Alfred Kempe found a proof for the sentence. Years later, 1890 , Percy Heawood showed eleven that Kempes proofwas incorrect. A second incorrect proof, published 1880 of Peter Tait, could long not be disproved likewise eleven years. Only 1891 showed Julius Petersen that also Taits was not correct proof. Heawood gave in the year 1890 with the refutationof Kempes four-color proof, additionally a proof for the five-color set on, with which an upper border for the colouring was proven for the first time error free by planar graphs. In Kempes incorrect proof passed already fundamental ideas, those through to the later proofAppel and hooks led.

Heinrich Heesch developed procedures in the 1960er and 1970er years, in order to look for a proof with the help of the computer.

Whereupon constructing Ken Appel and Wolfgang hook 1977 could find such. The proof reduced the numberthe problematic cases of infinite on 1.936 (a later version even 1,476), which were examined individually by a computer.

1996 could find Neil Robertson , Daniel of Sanders , Paul Seymour and Robin a Thomas's modified proof, to that the cases up633 reduced. Also these had to be examined by computers.

2004 designed Benjamin Werner and Georges Gonthier a formal proof of the sentence in the proof assistant Coq. Thus it is no longer necessary to trust the computer programs for the examination of the individual cases,separate “only” the Coq system.

The four-color set was the first large mathematical problem, which was solved by computers. Therefore the proof was not recognized by some mathematicians, since it cannot be reconstructed directly by humans. Finally must one on the correctness of the compiler and the hardware rely. Also the mathematical elegance of the proof was criticized (“a good proof reads itself like a poem - this looks like a directory!").

## formalizing

Representation of the formulation in the graph theory

formal can be described the problem most simply with the help of the graph theory. One asks whether the knots of each planar graph with maximally four colors be colored in such a way can that no neighbouring knots the sameColor carry. Or more briefly: “Is each planar graph 4-färbbar? “With it exactly one knot is assigned to each country of the map and for two knots, whose countries border, is connected.

The four-color problem is a special case of the Heawood assumption. The classical four-color problem concerns maps,on a level or a Kugeloberfläche lie. The “Heawood assumption” places the similar problem for general surfaces, for instance the Klein bottle (6 colors), the Möbiusband (6 colors), the Projektive level (6 colors) and the torus (7 colors). Interestingly enough is the Verallgemeinerung-- refrained from the special case for levels or Kugeloberflächen -- substantially more easily to prove than the four-color set and gets along without computer assistance. J. W. Ted Youngs and Gerhard Ringel could prove the Heawood assumption for all other cases in the year 1968 first times(Sentence of Ringel Youngs). The four-color set will thus not verified by this proof, but must separately be treated.

## remark

if (as in the reality frequently the case) a country is distributed on several non-adjacent areas(Colonies, enclaves, Exklaven,…), then the associated graph is not necessarily planar and it is possibly more than four colors for the colouring necessarily.