Slashdot Mirror
A Mathematical Proof Too Long To Check
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."
TL;DC
PlanetVulkan.com
In the results there is the following statement.
"As any idiot can plainly see"
If something is so important that you feel the need to post it on the internet... It probably isn't that important.
I guess we've moved on from using "Libraries of Congress" as a unit of data size. I wonder how many "less than Wikipedia"s worth of data the NSA has?
Apparently wizard is not a legitimate career path, so I chose programmer instead.
I have discovered a truly marvellous proof of this, which this DVD is too small to contain.
"Its size makes it unlikely that humans will be able to check and confirm the proof."
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."
I browse on +1 so AC's need not respond, I won't see it.
Editor? This is Slashdot.
"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
Editor? This is Slashdot.
You forgot to finish with the kick into the pit of death.
But what if GP is already using Beta?
Those who advocate genocide deserve every protection afforded by law, and none afforded by common human decency.