Has mathematics become an experimental science? Yes, according to the most prestigious journal of mathematics - at least that part of maths that involves computer proofs. It seems that some of the most famous problems in maths can only be solved with the assistance of computers, and the journal Annals of Mathematics has decided that the computer parts of these proofs are essentially uncheckable and should instead be thought of as similar to scientific experiments.
Whatever happened to the cut and dried world of maths, where either a mathematical theorem has been proved or it hasn't? Up until recently it was obvious what a mathematical proof should look like - a rigorous argument, consisting of a sequence of logical steps written on paper that any expert in the field could read, understand and believe. But the world of mathematics is changing, and this was highlighted at a discussion meeting about the nature of mathematical proof at the Royal Society last month.
Is this where the next great mathematical proof is?
Over the last 30 years a new breed of proof has emerged: one which relies on a computer to carry out part of the work alongside a more traditional mathematical argument. One of the most famous computer proofs is for the deceptively simple Four Colour Theorem, which states that four colours is enough to colour any map without having to use the same colour for any two adjacent countries. Originally conjectured in 1852, this theorem was finally proved in 1976 by Kenneth Appel and Wolfgang Haken. Their proof relied on a computer to check a large number of special cases and, according to Professor Robert MacPherson at the discussion meeting, a member of the editorial board of the Annals, "the reaction of the mathematical community was not universally positive. Some mathematicians thought that using a computer was cheating." (Read more about mathematical proof and the Four Colour Theorem in The philosophy of proof from Issue 10 of Plus.)
A test case
About a decade ago Annals decided that it was important to accept computer proofs in order to expand the type of mathematics that was publishable. MacPherson said the most compelling reason was that "there are interesting theorems that can only be proved using computers". Under the journal's policy of using teams of referees to check the computer sections thoroughly, Annals had successfully handled such proofs, despite this checking process taking longer than for a traditional proof.
Oranges stacked in the familiar face-centred cubic packing.
Annals approached Hales to submit his proof of this important result in 1998. It consists of 250 pages of conventional mathematical argument and over 3 gigabytes of computer code and data. MacPherson said they knew it would be a hard task, but they had hoped to build confidence in computer-assisted proofs by completely verifying Hales's proof of Kepler's Conjecture. "We failed," he said.
According to MacPherson, the refereeing effort was among the most massive he had come across. Annals hosted a conference to initiate the process, and a panel of 12 experts began work on verifying the proof in 1999. But eventually, after four years of trying, they had to throw in the towel. Gabor Fejes Tóth, the chief referee, reported that he was 99% certain of the correctness of the proof, but that they had been unable to completely certify its correctness. "It is not as if it hasn't been looked at," said MacPherson. "Everywhere they looked it was just as Hales said, but it was too hard to look at the whole thing." Trying to explain why the proof was so difficult to verify he quoted Ian Stewert's comparison of Hales' proof to the recent proof of Fermat's Last Theorem - "Wiles' proof of Fermat resembles War and Peace, but Hales' proof of Kepler resembles a telephone directory" - and it is almost impossible to check the correctness of every entry in a telephone directory.
The final decision is that Annals will publish the theoretical part of the proof, which has been checked successfully, but the computer section will be published separately in a more specialised journal. This was a disappointing outcome to what had seemed like a promising step towards gaining greater acceptance of computer proofs in mathematics.
But perhaps it is not so surprising that proofs of such a different nature will need to be assessed very differently. Annals has amended its policy on computer proofs, and will not now expect to verify the computer sections of proofs to the same thorough standard as it will continue to apply to the theoretical parts. Instead, computer proofs will be treated as more akin to experiments, which are accepted by referees if certain standards are met and consistency checks are satisfied.
Annals hopes to encourage others to re-prove such theorems, and to publish any new proofs that use different methods, even if they still require a computer. This approach brings mathematics closer to the experimental sciences such as chemistry and biology, where published work must adhere to high standards, but the results cannot be verified beyond doubt and the ultimate test is replicability.
At the discussion meeting, not all participants were worried by this new vision of mathematics. Professor Henk Barendregt from Radboud University in the Netherlands was optimistic about the use of computers as a new tool in mathematical proofs. He made a comparison with the use of microscopes in biology, which, among other advances, enabled scientists to discover cells, genes and DNA.
Who knows how computers may enhance mathematicians' vision in the future? But many will have been drawn to the subject in the first place by the concrete nature and beauty of a written proof. And those mathematicians may never be truly satisfied with a proof that no human can hope to understand.