Remember maps? In the old days, before smart phones and satnavs, we used to use them to get around. They posed quite a few problems, including folding them and understanding them. To help with the latter, map makers often use different colours to colour adjacent regions, be they countries, counties, or parts of a city. And pretty much since the beginning of map making, they have known that they will never need more than four colours to colour a whole map. It's something that's so blindingly obvious once you start playing with a few maps, it should be easy to prove mathematically: when colouring a map drawn on a flat piece of paper, four colours will always suffice.

The US in four colours. Image: Wikipedia.

Mathematicians first set themselves the task back in 1852, and it proved a massive headache. It took 24 years for the first proof to be announced, only to be found faulty another eleven years later. Then it took another 86 years, until 1976, until the mathematicians Kenneth Appel and Wolfgang Haken came up with a second proof. They first supposed that there are maps that need five colours, from which you can then choose one that has the smallest number of countries. They then showed that such a *minimal map*
must contain one of 1,936 possible configurations; and they also proved that every one of these possible configurations can be reduced into a smaller configuration which also needs five colours. This is a contradiction because they assumed that they had already started with the smallest five-colour map. When you find a contradiction you can deduce that your initial assumption, that there are maps that need five colours, is false.

This sounds good, but there was a hitch. The part of their proof which showed that these 1,936 configurations could be reduced was done by a computer, which simply ploughed through every configuration and checked it. No human being could in their lifetime ever actually read the entire proof to check that it was correct. This caused an outcry: if nobody can check it, how can we ever know it doesn't contain a mistake? Can mathematics ever be done by computers?

The proof has since been improved and verified independently (by computers), so most people are quite happy to consider the result proven. The question of whether computer proofs can ever be considered sound, however, is still a hot one.

To find out more, read The philosophy of proof and Welcome to the maths lab.

*Return to the Plus Advent Calendar*