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
less space than wikipedia? that sounds large.
wtf?
it is the beginning of AI-science, not the end of human science.
Science requires testable, provable, repeatable. If a human cannot understand the proof then he cannot participate in the science. This is likely to be referred to as an "early" version of machine-exclusive science.
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 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.
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?
Editor? This is Slashdot.
Gödel and Turing make strong cases that proving the algorithm works for some inputs that are correct proofs doesn't count as proof it will work for all correct proof inputs. So no, even if you "prove the algorithm works" it is not the same as a rigorous mathematical proof.
You're comparing apples to oranges (and lemons.)
If the algorithm can be proved correct (within whatever axiomatic system you're using) then it's correct. The End.
Gödel's incompleteness theorem shows that certain statements about axiomatic systems can be true but cannot be proved. That doesn't mean you can't be certain of something that is in fact proved (subject of course to the axioms.)
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.
If it weren't for deadlines, nothing would be late.
"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.
Proof is absolute, within the confines of the accepted axioms. Within the larger scope of things, we accept proof probabilistically, and this includes the entire works of every mathematician ever to live. Bayesian stats attempts to capture this idea that knowledge is never absolute, but merely held with probabilistic certainty, and all things are based on axioms (inherently unprovable, but assumed to be useful) ultimately. I only gripe (and boy is it a really fine, pedantic gripe), because your comment commits the same error you attack. Math/logic is a model, not reality. Models are based on necessary assumptions (axioms), otherwise you'd be arguing with solipsists over every detail, no matter how blindingly "obvious". This trend toward claiming that a mathematical proof or a scientific theory is "absolute" violates the very premise on which they're based.
No. If it's indeed a proof the probability of errors must be 0, not just close to it.
He's referring to errors during runtime (electrical noise, bit flips, not enough spiders in the case, etc.), not errors in the logic.
If the generator's logic is provably correct, then the things it generates are as well as long as your hardware it working properly. There is no way to rigorously prove hardware works correctly for all input strings, for all time, for all environmental conditions, across all variations due to manufacturing, etc.
"Yes, I have smoked crack cocaine."
Robert Ford, mayor of Toronto.
"If a nation expects to be ignorant and free in a state of civilization, it expects what never was and never will be."
I think the issue here stems from the concept of "correct" and how knowable that value is.
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.
If it weren't for deadlines, nothing would be late.
Also, unlike what you may think, a SAT proof is not a list of "I tried a=1 and it did not work out, and this is the proof that a=0". A standard SAT proof deduces new clauses from the original problem by applying the resolution rule repeatedly. The newly deduced clauses reduce the search space and, if the problem is unsatisfiable, the solver ends up with the empty clause, which is always FALSE. The proof is a collection of resolution steps that lead to FALSE.
SAT solvers are AI at least since:
SAT is clearly NP complete, and clearly the existence of good SAT solvers is not a proof that P=NP. This means that there will be relatively small problems that SAT solvers won't be able to solve. On the other hand, most real-world problems have a hidden structure which SAT solvers are able to find and use to their advantage.
The problem with this is that "axiomatic system" is an inadequate caveat. You also have to blindly assume that some specific system of deduction works. In practice, specific axioms are usually chosen based on the assumption that induction works, the basic unprovable assumption underlying all of science. But it's worse than that: you can't even prove that deduction works! (It's obvious in hindsight, really.)
Any logical system simply asserts rules of deduction. Why use some particular rules of deduction over another? Worse: humanity only realized recently that no such system can be both consistent and complete. What else are we missing?
So the best you can say is that a proof is or is not correct given arbitrary axioms and rules of deduction and we can't know in the general case whether a given proof is correct! Not much of a claim, really.
Socialism: a lie told by totalitarians and believed by fools.