Four color theorem
The four color theorem states the possibility of coloring (we also say coloring in graph theory) with four colors only a geographical map without two neighboring countries having the same color.
To be more precise, the Four Colors Theorem states that by using only four different colors, it is possible to color any map cut into related regions (in one piece), so that two adjacent regions (or bordering), that is to say having a whole border (and not just a point) in common always receive two distinct colors.
Thus, each of the regions should be given a different color if the regions are two by two adjacent.
Moreover, there cannot exist five adjacent two by two connected regions (this is the easy part of Kuratowski's theorem).
This four-color theorem has practical application in the assignment by a mobile operator of GSM frequencies to the coverage areas of base stations in its network. Indeed, as in the situation of the four colors:
- a GSM network is modeled, like a geographical map, by contiguous hexagons: each hexagon (called “cell”, hence the notion of cellular network) corresponds to the radiation of a base station (approximately 30 km in diameter in rural area).
- two contiguous hexagons must in no case be assigned the same frequency band.
History of the four color theorem
The first four-color conjecture seems to have been made in 1852 by a South African mathematician and botanist, Francis Guthrie (1831 - 1899).
Francis Guthrie was a student at University College London, where he studied with the famous De Morgan.
He then turned to studies of botany, while his brother, Frederick Guthrie, became a mathematician and also followed De Morgan's courses.
Francis Guthrie notices that four colors are enough for him to color the (however complex) map of the cantons of England, without giving the same color to two adjacent cantons (having a common border).
He then asks his brother Frederick, if this property would not be true in general for any flat map; the latter communicated the conjecture to De Morgan, and in 1878 Cayley published it.
- As early as 1879, Kempe found a first "proof" of the conjecture, but eleven years later Heawood found a major flaw in it; however, he will manage to find a five-color theorem.
A second "proof" by Tait in 1880 will likewise be refuted by Petersen in 1891.
- In 1913, the American mathematician George David BIRKHOFF (1884 - 1944), demonstrated the conjecture for all maps with less than 26 regions to be colored.
This terminal is improved during the XXe century.
- In 1969 Heesch found "almost" necessary and sufficient conditions for a configuration to be reducible, and a general method for finding an inevitable set of configurations.
The first computer-generated proof.
- Finally, in 1976, the American mathematicians Kenneth Appel (died April 19, 2013 at age 80) and German mathematician Wolfgang Haken carry out Heesch's program.
They show, using tens of thousands of figures, that any non-4-colorable map must contain one of the 1478 configurations, and, with 1200 hours of computation, that these configurations are reducible.
It's done the first computerized proof of a mathematical theorem.
- In 1995, Robertson, Sanders, Seymour and Thomas took advantage of the formidable acceleration of computers to find a much simpler realization of Heesch's program, with only 633 configurations; moreover they also automate the proof of inevitability.
- In September 2012, six years after the computer demonstration of the four color theorem, Georges Gonthier and his team succeeded in demonstrating Feit's theorem and Thompson. A theorem even more difficult to formalize.