A mathematical proof is irrefutably true, a manifestation of pure logic. But an increasing number of mathematical proofs are now impossible to verify with absolute certainty, according to experts in the field.
鈥淚 think that we鈥檙e now inescapably in an age where the large statements of mathematics are so complex that we may never know for sure whether they鈥檙e true or false,鈥� says Keith Devlin of Stanford University in California, US. 鈥淭hat puts us in the same boat as all the other scientists.鈥�
As an example, he points to the Classification of Finite Simple Groups, a claimed proof announced in 1980 that resulted from a collaboration in which members of a group each contributed different pieces. 鈥淭wenty-five years later we鈥檙e still not sure if it鈥檚 correct or not. We sort of think it is, but no one鈥檚 ever written down the complete proof,鈥� Devlin says.
Advertisement
Part of the difficulty is the computer code used nowadays to construct proofs, says Thomas Hales, at the University of Pittsburgh, Pennsylvania, US, as this makes the proofs less accessible, even to experts.
Stacking oranges
In 1998 Hales submitted a computer-assisted proof of the Kepler conjecture, a theorem dating back to 1611. This describes the most efficient way to pack spheres in a box, wasting as little space as possible. It appears the best arrangement resembles the stacks of oranges seen in grocery stores.
Hales鈥� proof is over 300 pages long and involves 40,000 lines of custom computer code. When he and his colleagues sent it to a journal for publication, 12 reviewers were assigned to check the proof. 鈥淎fter a year they came back to me and said that they were 99% sure that the proof was correct,鈥� Hales says. But the reviewers asked to continue their evaluation.
However, this tiny uncertainty did not disappear with time. 鈥淎fter four years they came back to me and said they were still 99% sure that the proof was correct, but this time they said were they exhausted from checking the proof.鈥�
As a result, the journal then took the unusual step of publishing the paper without complete certification from the referees (Annals of Mathematics Vol. 162, p. 1063-1183, 2005).
Automated checking
Even the review of proofs has come into the domain of computers, according to Devlin: 鈥淲e鈥檝e handed off some of the checking, some of the verification if you like, to computers.鈥� This has had some success, such as with the Four Colour Theorem.
The increased complexity is not necessarily all bad. 鈥淚f you want to solve a problem badly enough and you can do with a computer what you can鈥檛 do without a computer then of course you鈥檒l use it,鈥� says Hales.
And Devlin adds that all of this uncertainty about new proofs could be good for the discipline of maths: 鈥淚t makes it more human.鈥�
Devlin and Hales were speaking at the annual meeting of the American Association for the Advancement of Science in St Louis, Missouri, US.
