typodupeerror

## A Mathematical Proof Too Long To Check189

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."
This discussion has been archived. No new comments can be posted.

## A Mathematical Proof Too Long To Check

• #### To long, didn't check. (Score:5, Funny)

on Tuesday February 18, 2014 @01:44PM (#46278229)
TL;DC
• #### Re:To long, didn't check. (Score:2, Funny)

on Tuesday February 18, 2014 @01:47PM (#46278271)
Opps, "too long, didn't check." I guess I should have checked.
• #### After 9.5gigs (Score:5, Funny)

on Tuesday February 18, 2014 @01:51PM (#46278313)

In the results there is the following statement.
"As any idiot can plainly see"

• #### Re:wow (Score:5, Funny)

on Tuesday February 18, 2014 @01:52PM (#46278331)
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?
• #### Paging Mr Fermat... (Score:5, Funny)

on Tuesday February 18, 2014 @01:53PM (#46278351)

I have discovered a truly marvellous proof of this, which this DVD is too small to contain.

• #### Grad students? (Score:5, Funny)

on Tuesday February 18, 2014 @01:54PM (#46278361)
"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."
• #### Re:After 9.5gigs (Score:5, Funny)

on Tuesday February 18, 2014 @02:08PM (#46278549)

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)

by Anonymous Coward on Tuesday February 18, 2014 @02:23PM (#46278735)

Editor? This is Slashdot.

• #### Canadian Prime Minister would say... (Score:5, Funny)

on Tuesday February 18, 2014 @02:49PM (#46278993)

"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)

<[moc.liamg] [ta] [egdesuorbenet]> on Tuesday February 18, 2014 @03:03PM (#46279115)

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)

on Tuesday February 18, 2014 @03:28PM (#46279359)

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)

on Tuesday February 18, 2014 @04:10PM (#46279743) Journal

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)

<social@bronstrup.com> on Tuesday February 18, 2014 @04:31PM (#46279909) Journal
Or, considering the value of C... "Two long, didn't check" may be just as appropriate.

Another megabytes the dust.

Working...