A Mathematical Proof Too Long To Check 189
mikejuk writes "Mathematicians have generally gotten over their unease with computer-assisted proofs. But in the case of a new proof from researchers at the University of Liverpool, we may have crossed a line. The proof is currently contained within a 13 GB file — more space than is required to hold the entirety of Wikipedia. Its size makes it unlikely that humans will be able to check and confirm the proof. The theorem that has been proved is in connection with a long running conjecture of Paul Erdos in 1930. Discrepancy theory is about how possible it is to distribute something evenly. It occurs in lots of different forms and even has a connection with cryptography. In 1993 it was proved that an infinite series cannot have a discrepancy of 1 or less. This proved the theorem for C=1. The recent progress, which pushes C up to 2, was made possible by a clever idea of using a SAT solver — a program that finds values that make an expression true. Things went well up to length 1160, which was proved to have discrepancy 2, but at length 1161 the SAT returned the result that there was no assignment. The negative result generated an unsatisfiability certificate: the proof that a sequence of length 1161 has no subsequence with discrepancy 2 requires over 13 gigabytes of data. As the authors of the paper write: '[it]...is probably one of longest proofs of a non-trivial mathematical result ever produced. ... one may have doubts about to which degree this can be accepted as a proof of a mathematical statement.' Does this matter? Probably not — as long as other programs can check the result and the program itself has to be considered part of the proof."
To long, didn't check. (Score:5, Funny)
Re:To long, didn't check. (Score:2, Funny)
After 9.5gigs (Score:5, Funny)
In the results there is the following statement.
"As any idiot can plainly see"
Re:wow (Score:5, Funny)
Paging Mr Fermat... (Score:5, Funny)
I have discovered a truly marvellous proof of this, which this DVD is too small to contain.
Grad students? (Score:5, Funny)
I thought that's what grad students were for: endless mind-numbing labor. "Here, check this and have it back to me in 30 years or so."
Re:After 9.5gigs (Score:5, Funny)
I have it on good authority that one of the steps of the proof is "???", followed by "PROFIT!".
Re:"Less space ... to hold ... Wikipedia"?!?!? (Score:2, Funny)
Editor? This is Slashdot.
Canadian Prime Minister would say... (Score:5, Funny)
"A proof is a proof. What kind of a proof? It's a proof. A proof is a proof. And when you have a good proof, it's because it's proven."
Jean Chretien, former Prime Minister of Canada
Oh, so that's what Beta is for (Score:5, Funny)
Editor? This is Slashdot.
You forgot to finish with the kick into the pit of death.
But what if GP is already using Beta?
Re:To long, didn't check. (Score:5, Funny)
The neat part is that, if you take the first bit of each byte of the proof and string them all together, you get a complete HD MPEG copy of The Matrix.
Re:To long, didn't check. (Score:5, Funny)
So you say the real reason why they cannot check the proof is that they would violate the DMCA by doing so?
Re:To long, didn't check. (Score:4, Funny)