icon

The origins of proof IV: The philosophy of proof

Robert Hunt Share this page
January 2000
In this final article in our series on Proof, we examine the philosophy of mathematical proof.

What precisely is a proof? The answer seems obvious: starting from some axioms, a proof is a series of logical deductions, reaching the desired conclusion. Every step in a proof can be checked for correctness by examining it to ensure that it is logically sound, and you can tell that you've proved a theorem once and for all by making sure that every step is correct.

This might sound simple enough, but one problem is that humans (and even computers) are fallible: what if the person checking a proof for correctness makes a mistake and thinks that a step which is logically incorrect is in fact correct? Obviously somebody else will need to check that the person doing the checking didn't make any mistakes; and somebody will need to check that person, and so on. Eventually you run out of people who could check the proof: and in theory they could all have made a mistake!

The question "When is a proof not a proof?" is one which philosophers have debated for centuries. The problem is compounded by the fact that some proofs are so specialised that very few people in the world can even understand them; and some proofs are so long that very few people in the world have time to read them! In this article we shall explore some famous examples.

Too difficult for me

An exuberant Andrew Wiles.

An exuberant Andrew Wiles finally proving Fermat's Last Theorem.

Fermat's Last Theorem, a problem which has been around since 1637 when Pierre de Fermat wrote it into the margin of one of his books, was finally proved in 1993 by Andrew Wiles of Princeton University, USA, while he was visiting the Isaac Newton Institute for Mathematical Sciences in Cambridge. The proof is extremely intricate, and relies on the reader having studied the most modern and highly advanced number theory. It's also quite long, taking up over 100 pages in print. But only a handful of people in the entire world can understand the proof. To the rest of us, it's utterly incomprehensible, and yet we are quite happy to announce that "Fermat's Last Theorem has been proved". We have to believe the experts who tell us it has been, because we can't tell for ourselves.

In no other field of science would this be good enough. If a physicist told us that light rays are bent by gravity, as Einstein did, then we would insist on experiments to back up the theory. If some biologists told us that all living creatures contain DNA in their cells, as Watson and Crick did in 1953, we wouldn't believe them until lots of other biologists after looking into the idea agreed with them and did experiments to back it up. And if a modern biologist were to tell us that it were definitely possible to clone people, we won't really believe them until we saw solid evidence in the form of a cloned human being. Mathematics occupies a special place, where we believe anyone who claims to have proved a theorem on the say-so of just a few people - that is, until we hear otherwise.

In fact, the first proof of Fermat's Theorem which Wiles produced had a flaw in it. The mathematicians who checked his proof for errors with a fine-toothed comb found a gap in the proof, and insisted that it had to be corrected. It took Wiles another year to find a way of circumventing the error, so it wasn't until 1994 that a full complete and correct proof was published. Or was it? Nobody knows whether there might be another error lurking in his proof: the whole proof might be completely wrong. But for the moment we are happy to say that "it has been proved".

Map Colouring

An exuberant Andrew Wiles.

Part of the world map, coloured in more than four colours. The minimum number of colours required is four.

Another famous problem concerns everyday maps, such as the one above. Since map-makers started to colour maps, to show political regions such as different countries, they have known that you only ever need four colours. The rule for colouring in a map is that any two regions which share a border must be filled in using different colours. You soon find after playing around with a few maps that however complicated you make your map, you can always colour it with only four colours. Try it for yourself! (This is true as long as you don't require that two regions which don't touch must have the same colour, for example because they are members of an empire.)

An exuberant Andrew Wiles.

A simple map coloured correctly with four colours.

In 1852 this problem came to the attention of mathematicians who tried to prove that you never needed five or more colours. Up until then everybody had simply assumed that because they couldn't find a map which did need five colours, there must not be one.

The problem was found to be very difficult, but in 1879 an Englishman called Alfred Kempe announced his proof in both the magazine Nature and the American Journal of Mathematics. Thus the problem was solved and Kempe's proof was accepted far and wide. Unfortunately, in 1890, 11 years later, Percy Heawood found an error in the proof which nobody had spotted despite careful checking. So the problem returned to being unsolved, and it was another 86 years before the matter was settled.

In 1976, Kenneth Appel and Wolfgang Haken finally managed to prove the theorem for a second time. They used some of Kempe's ideas, but avoided his mistake. They assumed that there was in fact a map which needed five colours, and proceeded to show that this lead to a contradiction, as follows. If there are several five-colour maps, then choose one with the smallest number of countries: this is known as the "minimal criminal" for obvious reasons! Appel and Haken proved that this 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 we assumed that we already started with the smallest five-colour map.

Cartoon

However, the part of their proof which showed that these 1,936 configurations could be reduced was actually done by a computer, which simply ploughed through every configuration and checked it. The proof, if printed out by the computer, would take reams and reams and reams of paper: no human being could in their lifetime ever actually read the entire proof to check that it was correct. Several mathematicians of the time complained that this meant that it wasn't really a proof at all! If nobody could check the proof, how could we ever know whether it was right or wrong? So not everybody is convinced that the four-colour theorem has really been proved.

More recently, in 1996, Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas came up with a simpler proof involving only 633 configurations. It still needs a computer though, so the problem remains!

Kepler's Conjecture

Packing oranges.

Packing oranges.

In Issue 3 we reported on Kepler's conjecture, which states that the best way to pack spheres together so as to fit in as many as possible is to use the so-called face-centred cubic packing - better known as the way that greengrocers pack oranges. In 1997 when we published our story, nobody had managed to prove the conjecture, though it looked as if progress was imminent.

Wu-Yi Hsiang of the University of California at Berkeley had published a proof in 1990, but it had errors. Despite his repeated attempts to fix these errors, he could never correct his proof. Now he's been beaten to it by Thomas Hales of the University of Michigan who has published a 250-page proof. But even if you manage to plough through those 250 pages you still need to use a computer to check out some of his inequalities. Is this a proof?

Jobs for Philosophers

Philosophers and mathematicians will have to decide precisely what a proof really is. It looks as if "proofs by computer" are here to stay, and we're going to have to live with them whether we like it or not! And the problem of knowing whether the people who check our proofs for errors have made errors themselves will never go away. Some would say that computers are actually less likely to make errors than humans! And anyway, Gödel showed us that it is impossible for us to even know whether basic arithmetic is self-contradictory or not, which seems to make the whole question somewhat academic.

For the present, we'll have to live with all these problems. But next time somebody comes to you and tells you that they've proved something - and here at Plus, we get people saying just that to us every month - say to them: "Ah, but what do you mean by a proof?"

Further Reading


About the author

Dr. Robert Hunt is the Editor of Plus Magazine. He is a Lecturer in the Department of Applied Mathematics and Theoretical Physics at Cambridge University, and a Fellow of Christ's College.