This site contains my notes about searching a pencil and paper proof of the four color problem. This problem, stated in terms of graph theory, that every loopless planar graph admits a vertex coloring with at most four different colors, was proved back in 1976 by Appel and Haken, using a computer. It was the first major theorem to be proved using a computer. Many people are still trying to solve it the old way.
Martin Gardner commented: “Whether a simple, elegant proof not requiring a computer will ever be found, is still an open question. It’s interesting that such a simple, intuitive puzzle can be so difficult to settle!”
- Around this date, I started experimenting a new method based on Kempe’s chains. Read the blogs I published starting from this one:
Notes taken before November 2016.
The approach used here to find a new solution is also based on two results which, I think, haven’t been considered so far:
- T1) All regular maps can be simplified by removing all faces with less than five edges, without affecting the search and the validity of the proof. In other words, only maps with all faces with five or more edges can be considered when searching for a demonstration of the problem. 02/Apr/2011 – This theorem was already known. See T1 for details.
- T2) All regular maps can be topologically tranformed into circular or rectangular maps, which are (non only visually) more manageable forms of maps
This picture shows on the first row some maps I found on web pages dedicated to the four color theorem and on the second row how these maps could have been represented (just an example to show the representation) using circular and rectangular maps.
For example Tutte’s map can be represented as shown here. Face number 25 surrounding all the other faces on the original map, is the ocean of the rectangular and circular maps.
Tutte’s map converted into circular and rectangular (using different colors):
Other examples of maps represented as circular and rectangular mode, uncolored and colored, are presented here: