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
Don't a lot most of what's said which is why i'm interested in this!
less space than wikipedia? that sounds large.
wtf?
This proof has been Computer Certified to be 100% correct and complete. That's all I need to see to believe it. Now I'll just turn in my homework to my mathematics prof on the portable hard drive.
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.
hey matermerticians : GIGO
"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.
Sounds like a bad idea to me, a civilian. It reminds me of the old saw about the man who "knows nearly everything about almost nothing."
Unless world population continues to rise exponentially, I fear this proof is doomed to oblivion for lack of anyone who cares and has the ability to check 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.
First, assume that we have an infinite supply of mathematicians hitting random keys on a computer for a limited amount of time. Then we _know_ that they will almost surely find the proof:
http://en.wikipedia.org/wiki/Infinite_monkey_theorem
"Less space than is required to hold the entirety of Wikipedia"
Wikipedia download, currently 9GB compressed and 44GB uncompressed.
So technically correct, but completely useless for comparison? "this file so big -this other file is even bigger than it!"
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.
The bottom /. quote for me reads as follows -
"Everything should be made as simple as possible, but not simpler." -- Albert Einstein
"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 am looking forward for the moment, when computer will generate a nontrivial theorem 13GB long and prove it so that no human will be able to undertand the theorem, not even the proof.
Human
Math hypothesis
Computer
??
??
??
??
Proof!
?
?
?
Profit!!!!
Let's see. If I can read a 500 page book in a day, it would ONLY take me 35.6 years to read the proof! And that says nothing about proving/disproving/understanding it! :rolleyes:
Many eyes make a shallow proof. Just have everyone check one step, and the whole proof will be checked in no time.
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.
Be right back.
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.
As a result all SAT solver implementations are heuristic approximations of a true SAT solver.
How do they account for this in the paper?
At least that dammed Beta is not popping up!At least that dammed Beta is not popping up!
Back to a nice user friendly Slashdot.
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
Amazon's mechanical turk to the rescue!
I take it this proof was produced by AFRICANS, since 'they are just as intelligent as other races', and 'We are all the same'?
What's that you say? There aren't any African maths geniuses? How can that possibly be? The TV told me we are all the same!
Fuck Slashdot and fuck the Beta. I hope people at DICE have a terrible cancer-induced deaths, along with all their families.
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.
Why not use the rigorous method used to prove the existence of global warming:
Just state that it's true and that anyone who disagrees is an idiot.
That's how I measure girls
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.
My comments won't even post. Fuck beta.
There was an error in page 3.
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
Where's my anti-gravity! Movies promised me anti-gravity and fusion. I know you're almost there on the fusion thing but I want my darned pink hoverboard. I think the lack of hoverboards causes all the problems of the world today. Who could question you if you were hovering over their heads with a rod that shot electricity?
P.S. I know you're not a physicist and the lack of this stuff isn't really your fault but all this stuff starts with the pure math so....I'm blaming you
Furlongs are the standard arbitrary unit of distance. Or maybe parsecs. Or chains.
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.
I don't know if anybody will read this far down, but the topic has already been "done" with the Four Color Problem, in which a mechanical proof, too long for a human to review in a lifetime of work, was necessary to show that "four colors suffice".
because papers have shown that most programming problems occur in the same part of the program (either because of requirements understanding or common misconceptions).