University Maths Notes: Topology – The Four Colour Mapping Theorem
The four colour mapping theorem states that, given any separation of a plane into contiguous regions, no more than four colours are required to colour the regions of the map so that no two adjacent regions have the same colour. Two regions are called adjacent only if they share a border segment, not just a point. The theorem is illustrated below for the mainland USA.
In 1976, the theorem was apparently proved by Wolfgang Haken and Kenneth Appel at the University of Illinois with the aid of a computer. It was the first major mathematical proof proved substantially by computer. The program that they wrote was thousands of lines long, took over three years to write and took over 1200 hours to run. Since that time, a collective effort has been under way to check the program.
The proof of the four colour mapping theorem raises interesting questions about the relationship between people and computers as far as maths is concerned. Mathematicians think the most aesthetic proofs to be the most legitimate. These are at the moment the product of the human brain. People can make great leaps of logic and bring together things previously unconnected to construct often long and intricate proofs. All computers can do at present is exhaust all the possibilities, and if the programs they run contain errors, the results of thse programs will be unreliable, though the computers will never know.