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.
Just saying.
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?
less space than is required to hold the entirety of Wikipedia
WTF? Editor! Where's the EDITOR?
One trick is to use a completely different algorithm to generate it, if that is possible. I've done that many times in the past and they end up debugging each other. When they can churn for days always spitting ot identical results, you gain confidence.
(-1: Post disagrees with my already-settled worldview) is not a valid mod option.
I don't see why you need to go through the fuss of the 13 GB file. What was the algorithm used to make the file? Prove that the algorithm works. That's your proof. (Run the program a few times, so the probability of errors in the output is close to zero. Remember that the probability of the computer making a mistake (cosmic rays, transistor noise, etc) is smaller than the probability of a human mathematician making a mistake.)
" Prove that the algorithm works. That's your proof. (Run the program a few times, so the probability of errors in the output is close to zero"
"probably true" is NOT a prove.
I don't trust solvers. I've tried several "state of the art" and "award winning" solvers only for them to throw up on test inputs intentionally designed to mess with them after realizing I was way over my head attempting to roll my own.
Even working simple graphs expressed as a series of disjunctions A -> B -> C -> D (!A || B) && (!B || C) && (!C || D) yield garbage on a couple open source "crypto" branded solvers. I hope with the commercial solvers it is the case you get what you pay for... it seems the more exotic algorithms they use to beat NP the more fragile they become.
SAT solving is easy when there is a solution. When there is not, it gets very hard, as basically the solver enumerates all ways it could have found a proof and shows for each that it did not work. Still faster than a full exhaustive search (which is infeasible from, say 80 bits or so of problem space size). On the other hand, SAT solvers are not that complicated if you ignore implementation details. So the solver itself, together with the 1-bit answer "no" could be used as proof instead of the 13GB. My guess is that it will take some time for that to become accepted, but some mathematicians are pretty mentally agile and not opposed to use of modern tools at all.
Most ACs are not even worth the keystrokes to insult them. Be generically insulted by this and ignored otherwise.
The only person dumber than a moderator that didn't understand that reference, is the person who comments on moderation after only 19 minutes.
Slashdot social media options: AIM, ICQ, Yahoo, Jabber and Mobile Text. Why no MySpace?
And yes, it's computer proofs all the way down.
I eat only the real part of complex carbohydrates.
"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
Turns out its just a memory dump from when a processor bug caused a kernel panic.
The process, its results, and how its handled by humans will be an early example of decisions surrounding machine intelligence, in what will be the norm in the not-so-distant future.
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.
Oh its really quite simple.....once you've learned basic English.
Keep at it. I'm sure you'll get there eventually.
"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."
You presume the proof has unique steps at every point. It doesn't, if something couldn't be found in a random sequence of 1161 numbers, then it couldn't be found in an infinite sequence (my apologies for paraphrasing, go read the article). So they used a computer to check the 1161 numbers. So they essentially had a for loop. The code for the for loop was finite. The loop was finite. A few invariants and a bit of Floyd-Hoare logic and whallah, the proof be checked, just not the usual way you'd expect.
"whallah"? Really?
Socialism: a lie told by totalitarians and believed by fools.
My only questions are is it possible to simplify the proof? And how hard would that be?
If we have a testable proof, then it should be possible to throw another algorithm on it to simplify and optimize it...
Only after that step should it be considered ready to inspect and test by others.
Hmm, the humour and sarcasm seem to have been be lost on you.
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.
So how long will it take to check if you give it to 1000 people and let each one check 6500 pages?
The Tao of math: The numbers you can count are not the real numbers.
Dammit. I have a Bacon number (2). Now I have to go get my PhD and try to get an Erdos number. I can't beat the current lowest Erdos-Bacon number (4, held by Steven Strogatz), but I could tie it. Unless...If I can get onto a movie with Bacon himself in it, that might put 3 in striking range.
Where is "The Nth Degree" Barclay when you need him!AA
No problem -- just give it to Nancy Pelosi. She'll make sure it gets passed; and then you can find out what's in it. Congress doesn't read the bills is passes, why should mathematicians think they are so much better? ;^J
As a mathematician, the length of the certificate is the least interesting thing about this. 13G isn't big for a computer, 13K would be far too large for a human to check by hand, so this is not in any essential way different from any other proof using computer calculation.
The problem itself is fascinating, though; the N = 1 case is small enough to do by hand (I get 11 as the length of the longest sequence with no discrepancy greater than 1). Strange that they seem to think the N = 3 result may be less than 20000.
SAT solvers usually guarantee that their result is correct. What they don't guarantee is that they finish in reasonable time for every input.
I was trying to draw a distinction between problems that are beyond human comprehension and those that are merely beyond human time and ability, with huge SAT instances falling into the latter category.
Exactly, the use of SAT unsatisfiability certificates is just a proof strategy... Just like reductions used to show complexity classes, nobody comprehends all of them...
...why can't they just get their slaves, I mean graduate students, to check its validity by hand?
Please tell me the browser cache is screwing with me. Please tell me that my wife wants to have sex more often ( ok that isn't going to happen, I have a 12 and 15 year old) Do we really have Slashdot.org back?
Just give the file to Spock. Or Thufir Hawat.
There are other theorems with computer-assisted proofs that are too complex to verify by hand, going back decades. The four colour map theorem and the classification of finite simple groups are two examples.
Too long for peer review; Claim Rejected.
Okay, so the proof in the article may be too lengthy to accurately check, so why not work with something simpler.
For that, I present the proof that Pi R Square is incorrect.
1: Write down on a piece of paper the commonly used 3 digit shortened approximation of Pi: 3.14
2: Hold that paper up in front of a mirror.
3: Note that in reverse, the characters 3.14 now look like PIE.
4: Pie is typically round, therefore since Pie is round, PI.E is 3.14 backwards, and 3.14 is the common shortened value of Pi, then Pi R round, not square.
This space unintentionally left blank.
of this which is shorter. Unfortunately this comment field is too small to contain it.
I was trying to classify the normal subgroups of PSL(n,q) where n,q may be nonstandard elements of a nonstandard model of arithmetic. I pointed out that if Ariah Lev's work formalised correctly, then a few steps would yield the result I wanted, but that this was beyond checking. Once the PhD was done, I did further investigation, and scribbled a thought in a moment of insight, and left it to tidy itself up. I believe I put an entry on either chalisque.wordpress.com or deardiary.chalisque.org, but forget which, and am hunting it down. If not, John's Antibang Theory That Really Works and its notion of True Computability vs Turing equivalent non-True forms will see the light of day in a readable format, but if you want to know how my mind really thinks, this is a clue as to my mind's native language. It's quasi-English pseudo-maths that I then filter for correctness before communicating.
I can't find it, but there are a great many thoughts I had to dump out to reclaim brainspace. As a free software believer, and a free-thinking believer, I treat my programs and thoughts like a mother treats her children, caringly and lovingly and I don't send them out into the world ill-equipped to face rigorous challenge.
John_Chalisque
But is he is or is he isn't correct?
A most overlooked advantage to owning a computer is if they foul up there's no law against wacking them around a bit.
Or we can all just agree that it's probably right and move on to something else.
A most overlooked advantage to owning a computer is if they foul up there's no law against wacking them around a bit.
because papers have shown that most programming problems occur in the same part of the program (either because of requirements understanding or common misconceptions).