Mathematical proofs getting harder to verify
12:29 19 February 2006
NewScientist.com news service
Roxanne Khamsi, St. Louis

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.

"I think that we're now inescapably in an age where the large statements of mathematics are so complex that we may never know for sure whether they're true or false," says Keith Devlin of Stanford University in California, US. “That 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. "Twenty-five years later we're still not sure if it's correct or not. We sort of think it is, but no one's ever written down the complete proof," Devlin says.

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. "After 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. "After 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: "We've 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. "If you want to solve a problem badly enough and you can do with a computer what you can't do without a computer then of course you'll use it," says Hales.

And Devlin adds that all of this uncertainty about new proofs could be good for the discipline of maths: "It 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.

I dont know you, but Im gonna go out on a limb and say that...Its been a while you need to get laid.  Why on earth are you posting this on a Saturday night?

to each his own though

I hate it when reporters try to report on things.  It always ends badly.  If it can't be verified, then it isn't a proof.  By definition.  The issue here is that people are using computers to construct massive truth tables.  It is kind of a second rate proof technique anyway, but in order to use this to prove a mathematical statement, you have to be sure you've covered every case.  Hard to do when you're talking about the correctness of computer software and hard to do on large problems.  

Must not be much work for mathematicians if they are stacking oranges.

He should be spending more time on the whole 42 thing.

I don't think they found a proof of the four-color; I seem to recall they just used a computer to try every possible combination (and yes, there was an amazingly-large number of combinations). That is a test, not a proof.
~

Quoted: I don't think they found a proof of the four-color; I seem to recall they just used a computer to try every possible combination (and yes, there was an amazingly-large number of combinations). That is a test, not a proof. ~

Somethings in Mathematics are impossible to prove (for example proving orbital stability in a system that has more than 3 bodies, for an infinite period of time: ie is the Solar System Stable?), other things (called Conjectures) such as Goldbach's Conjecture or Reimann's Hypothesis are simple statements but like Fermat's Last Theorem: incredibly difficult to prove.

Okay, where's the pic showing the mathematical proof that girls are evil?  Somebody post that, pleeeease!    MJD

Quoted: I don't think they found a proof of the four-color; I seem to recall they just used a computer to try every possible combination (and yes, there was an amazingly-large number of combinations). That is a test, not a proof. ~

It's an amazinly ugly proof, but it is a proof. Actually, there's an infinite number of cases; they reduced it by reasoning down to some 4000-odd cases which they then fed to a computer.