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

wow

[Anonymous Coward]

less space than wikipedia? that sounds large.

wtf?

Re:the beginning, not the end

[Kufat]

I'd hesitate to call one big for loop "AI." The interesting part of the proof is the reduction to SAT, and that's easily understood by mathematicians. The computer part is a straightforward and dull brute force search.

Less space than Wikipedia

[BlueMonk]

less space than is required to hold the entirety of Wikipedia

I'd venture a guess that this is not unique and that every mathematical proof to date takes less space than Wikipedia. Did they mean more space?

Re:wow

[Nexus7]

I think they meant to say "less space than that is required to store Wikipedia".

Re:wow

[tsqr]

I think they meant to say "less space than that is required to store Wikipedia".

Probably not. Since 0 bytes is less space than that is required to store Wikipedia, I would wager that they actually meant to say, "more space than that is required to store Wikipedia.

Re:wow

[egcagrac0]

AFAIK, a "standard" LoC is 10TB... around 769 times larger than this file. Comparing this to an LoC is technically valid, but not particularly useful for the typical reader.

Re:To long, didn't check.

[Garridan]

Mathematicians are supposed to be able to think at a higher level of abstraction than most other folks. Any mathematician who claims that 'this is too much for a human to check' is an idiot. It's not too much. We understand how computers work. They're way less error-prone than humans.

1) Verify the proof that the verification algorithm works.
2) Obtain several independent simple, portable implementations of said verification.
3) Run said implementations on proof certificate on a variety of hardware.

Trust the math, and where it comes to the hardware and software, trust but verify. Too long to check without aid of a computer? Sure, I'll buy that. But you'd have to be an idiot to want to check this proof without a computer. Why is this news? (actually, the result in discrepancy theory is wonderful, and I'm very happy to see it here on Slashdot... but massive computer proofs are truly nothing new)

Re:prove that the program works

[ClickOnThis]

I think the issue here stems from the concept of "correct" and how knowable that value is.

Turing's halting problem is a statement about limitations in the ability of algorithms to examine other algorithms. Again, it doesn't mean you can't prove that an algorithm is correct, no matter how "correct" the algorithm appears.

Um, excuse me. If you're going to quote me and change what I said, then indicate your edits. I have done so above, in bold. Not that I can make sense of them.

That's kind of my point. Given this proof, it would show that the algorithm is incorrect if the proof is shown to be invalid

Wha...? That's just plain wrong. I can think up all kinds of invalid proofs of the Pythagorean Theorem. But showing that a proof is invalid does not mean the theorem is incorrect. It just means your proof is.

yet the proof is too long to be verified by anything but another algorithm, so the halting problem is definitely relevant in a discussion about algorithm-generated proofs which can't be verified by humans.

Again, Turing's halting problem illustrates limitations on the ability of algorithms to decide certain propositions. It does not mean that algorithms can't decide anything. You seem to think that it does.

Yes, some proofs can be generated by algorithms and others can be checked by algorithms, but a mathematician is necessary at some point in the process since no non-trivial generating algorithm can be shown to create only correct proofs and no universal checking algorithm can be created which generates no false positives or negatives.

Your fallacy is that one cannot trust specific algorithms to prove things because no such universal algorithm can be created.