Beta
×

Welcome to the Slashdot Beta site -- learn more here. Use the link in the footer or click here to return to the Classic version of Slashdot.

Thank you!

Before you choose to head back to the Classic look of the site, we'd appreciate it if you share your thoughts on the Beta; your feedback is what drives our ongoing development.

Beta is different and we value you taking the time to try it out. Please take a look at the changes we've made in Beta and  learn more about it. Thanks for reading, and for making the site better!

A Mathematical Proof Too Long To Check

Soulskill posted about 7 months ago | from the which-this-margin-is-too-narrow-to-contain dept.

Math 189

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

cancel ×

189 comments

Sorry! There are no comments related to the filter you selected.

To long, didn't check. (5, Funny)

fleabay (876971) | about 7 months ago | (#46278229)

TL;DC

Re:To long, didn't check. (3, Funny)

fleabay (876971) | about 7 months ago | (#46278271)

Opps, "too long, didn't check." I guess I should have checked.

Re:To long, didn't check. (1)

maxwell demon (590494) | about 7 months ago | (#46279675)

Opps, "too long, didn't check." I guess I should have checked.

ITYM: Oops ...

SCNR

the computer's always right and other such quaint (0)

Anonymous Coward | about 7 months ago | (#46278355)

hey matermerticians : GIGO

Re:To long, didn't check. (5, Informative)

Garridan (597129) | about 7 months ago | (#46278583)

Funny thing about this. They've checked it. Actually, their "check" of this proof is many of orders of magnitude more rigorous than when, for example, a reviewer "checks" a math paper for errors before firing off a positive review. Nondisclaimer: I'm a mathematician.

Re:To long, didn't check. (3, Informative)

K. S. Kyosuke (729550) | about 7 months ago | (#46279139)

My understanding is that checking an output of a proof assistant/generator is a trivial matter (i.e., a trained monkey should be able to do it). It's just that it's a lot of data even for the most patient humans in this case.

Re:To long, didn't check. (5, Insightful)

Garridan (597129) | about 7 months ago | (#46279641)

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:To long, didn't check. (1)

maxwell demon (590494) | about 7 months ago | (#46279727)

Who says it must be checked by a single human? In the extreme, each single step could be verified by a different human. And that even in parallel.

And even if it takes a century for humans to check that proof, it doesn't mean it's impossible. Unless we have a conclusive proof that humanity will not last that long.

Re:To long, didn't check. (4, Funny)

SydShamino (547793) | about 7 months ago | (#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. (5, Funny)

maxwell demon (590494) | about 7 months ago | (#46279743)

So you say the real reason why they cannot check the proof is that they would violate the DMCA by doing so?

News for nerds (1)

dysmal (3361085) | about 7 months ago | (#46278263)

Don't a lot most of what's said which is why i'm interested in this!

Re:News for nerds (1)

cheater512 (783349) | about 7 months ago | (#46279199)

Oh its really quite simple.....once you've learned basic English.

Keep at it. I'm sure you'll get there eventually.

wow (5, Insightful)

Anonymous Coward | about 7 months ago | (#46278277)

less space than wikipedia? that sounds large.

wtf?

Re:wow (5, Funny)

HaZardman27 (1521119) | about 7 months ago | (#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?

Re:wow (-1)

Anonymous Coward | about 7 months ago | (#46278465)

I wonder how many "less than Wikipedia"s worth of data the NSA has?

A couple of GB of "My Friend's Hot Mom" porn.

Re:wow (1)

gnick (1211984) | about 7 months ago | (#46278563)

We're getting to a point where, "Can I store it on a card smaller than my pinky nail?" has replaced "Libraries of Congress."

Re:wow (0)

Anonymous Coward | about 7 months ago | (#46278693)

I thought it was Volkswagens for a while. All these changes in measurement make me wish for the good old days when we used cubits.

Re:wow (1)

SJHillman (1966756) | about 7 months ago | (#46278831)

I always measured in station wagons. Maybe that's the American equivalent of a Volkswagen.

Re:wow (1)

Garridan (597129) | about 7 months ago | (#46279659)

Maybe out in Granola Country. Where I'm from, we measure in Hummers.

Re:wow (1)

maxwell demon (590494) | about 7 months ago | (#46279761)

I thought it was Volkswagens for a while. All these changes in measurement make me wish for the good old days when we used cubits.

Don't worry, when we have quantum computers on our desks, we will use qubits. Almost the same as cubits, isn't it? ;-)

Re:wow (3, Insightful)

egcagrac0 (1410377) | about 7 months ago | (#46279297)

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:wow (1)

EvilSS (557649) | about 7 months ago | (#46278335)

less space than wikipedia? that sounds large.

wtf?

Yea, checking TFA it appears this is a case of less = more.

Re:wow (0)

Anonymous Coward | about 7 months ago | (#46278463)

The proof that 1=1 also takes "less space than is required to hold the entirety of Wikipedia"

Re:wow (1)

Anonymous Coward | about 7 months ago | (#46279071)

1=1 does not require a proof because it is an axiom, also known as a formalized assumption. This is sometimes referred to as the Identity Axiom.

Re:wow (0)

Anonymous Coward | about 7 months ago | (#46279097)

And even 0 space is less than required to store wikipedia.

Re:wow (1)

Anonymous Coward | about 7 months ago | (#46279355)

Depends on what set of axioms you pick as your base set, and some common choices don't have have that as an axiom because it is (easily) provable from a more basic set of axioms. For example, using something similar to Tarski's set of predicate calculus axioms requires something like 9 steps [metamath.org] if being explicit.

Re:wow (3, Insightful)

Nexus7 (2919) | about 7 months ago | (#46278565)

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

Re:wow (1, Insightful)

tsqr (808554) | about 7 months ago | (#46279037)

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.

Computer Certified! (TM) (0)

Anonymous Coward | about 7 months ago | (#46278283)

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.

the beginning, not the end (5, Interesting)

EngineeringStudent (3003337) | about 7 months ago | (#46278311)

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.

Re:the beginning, not the end (0)

Anonymous Coward | about 7 months ago | (#46278439)

Why can't we get thousands of mathematicians to take on a part of the proof and check it that way? Or is that impossible?

Assume that we have an infinite supply of mathemat (0)

Anonymous Coward | about 7 months ago | (#46278887)

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

Re:the beginning, not the end (5, Insightful)

Kufat (563166) | about 7 months ago | (#46278453)

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.

Re:the beginning, not the end (0)

Anonymous Coward | about 7 months ago | (#46279591)

The computer part is a straightforward and dull brute force search.

Yes and no. The optimizations that most SAT solvers use to find truth conditions are impressive. However, to show a false condition, it is required to try everything.

SAT is not a brute force loop (5, Informative)

Mask (87752) | about 7 months ago | (#46279687)

As someone nearing the completion of his Ph.D. in a subject close to SAT I can say that SAT does not resemble "one big for loop", not a bit. A modern SAT solver can solve problems with millions of variables and hundreds of thousand clauses. In contrast, a brute force for loop would require O(2^N) iterations where N is in the millions, which is like eternity. As an exercise, please try to write a trivial solver that can handle even 100 variables.

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 [wikipedia.org] deduces new clauses from the original problem by applying the resolution rule [wikipedia.org] 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:
  • 1. They employ search (not unlike chess game).
  • 2. They have non-trivial heuristics (not unlike chess game).
  • 3. The heuristics evolve and improve over the course of a run.
  • 4. They are able to deduce new clauses from the original problem.
  • 5. Many solvers employ a lot of smarts to simplify the problem even before starting search.

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.

Re:the beginning, not the end (2)

maxwell demon (590494) | about 7 months ago | (#46279817)

I'd hesitate to call one big for loop "AI."

So you would more readily accept a big while loop as AI? ;-)

Re:the beginning, not the end (2, Informative)

Anonymous Coward | about 7 months ago | (#46278941)

It's far from the beginning. That would be in 1976 with the computer proof of the four color theorem [wikipedia.org] , which was the original controversy over proofs only checkable by a computer. The 13GB proof is certainly huge, but proofs that a human can't check aren't new. I don't know how it is in mathematics, but in programming languages research, any proof that isn't computer-checked is suspect because humans are just really bad at being completely consistent at long repetitive processes like checking proofs.

Re:the beginning, not the end (1)

DriedClexler (814907) | about 7 months ago | (#46279657)

Agree in principle, but I'm not sure this fails that standard to the extent that it's relevant for science to work. Sure, a human may not directly understand the entire proof. However, like with the Four Color Theorem, they can verify:

- A proof checker would catch errors if there were any, and has failed to.
- The thing it purports to prove is in fact (a representation) of the theorem the submitter claims to have proven.
- The proof generator generates only valid steps.

Could there be errors in the process? Sure. But it's definitely something that humans can do science with.

After 9.5gigs (5, Funny)

jellomizer (103300) | about 7 months ago | (#46278313)

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

Re:After 9.5gigs (1)

Trax3001BBS (2368736) | about 7 months ago | (#46278461)

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

LOL!
no, I didn't rta.

Re:After 9.5gigs (4, Funny)

QilessQi (2044624) | about 7 months ago | (#46278549)

I have it on good authority that one of the steps of the proof is "???", followed by "PROFIT!".

Paging Mr Fermat... (5, Funny)

UdoKeir (239957) | about 7 months ago | (#46278351)

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

Fags (-1)

Anonymous Coward | about 7 months ago | (#46278605)

Comment is not redundant and is funny. Though, he should have quoted the entire things with the DVD spin:

I have discovered a truly remarkable proof of this theorem which this DVD is too small to contain

You dumb faggots that mod comments on this site are sad.

Re:Fags (1)

mwvdlee (775178) | about 7 months ago | (#46278953)

The only person dumber than a moderator that didn't understand that reference, is the person who comments on moderation after only 19 minutes.

Grad students? (5, Funny)

EvilSS (557649) | about 7 months ago | (#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."

Say, what? (0)

Anna Merikin (529843) | about 7 months ago | (#46278397)

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.

Re:Say, what? (1)

gtall (79522) | about 7 months ago | (#46279231)

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.

Re:Say, what? (1)

lgw (121541) | about 7 months ago | (#46279315)

"whallah"? Really?

Can't have your pi and eat it too, (1)

Trax3001BBS (2368736) | about 7 months ago | (#46278435)

Just saying.

Less space than Wikipedia (5, Insightful)

BlueMonk (101716) | about 7 months ago | (#46278469)

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:Less space than Wikipedia (-1)

Anonymous Coward | about 7 months ago | (#46279135)

I believe they are saying that Wikipedia takes less than 13 gigabytes to store; context is key. They did it right.

Re:Less space than Wikipedia (0)

Anonymous Coward | about 7 months ago | (#46279533)

No, I think the poster has it correct. It is very difficult to read otherwise

Re:Less space than Wikipedia (1)

Anonymous Coward | about 7 months ago | (#46279585)

No, I think they are saying that Wikipedia is more than 13 GB but that the amount of space this proof requires is comparable to the amount of space stored by Wikipedia even though it needs less space.

(skipping car analogy).

It's like saying that our star is smaller or bigger than another star (insert star name here). The comparison is a fair one. But saying that the (planet or whatever it's called now) Pluto is smaller than the sun is a pointless statement. Or saying that the Earth is smaller than the sun. Saying that Mercury is smaller than Earth makes sense.

For instance, if the proof were a megabyte then there is no point in saying that the file is smaller than Wikipedia because a megabyte is not large enough to meaningfully compare it to Wikipedia by analogy.

"Less space ... to hold ... Wikipedia"?!?!? (1)

Anonymous Coward | about 7 months ago | (#46278493)

less space than is required to hold the entirety of Wikipedia

WTF? Editor! Where's the EDITOR?

Re:"Less space ... to hold ... Wikipedia"?!?!? (2, Funny)

Anonymous Coward | about 7 months ago | (#46278735)

Editor? This is Slashdot.

Re:"Less space ... to hold ... Wikipedia"?!?!? (0)

Anonymous Coward | about 7 months ago | (#46278947)

Editor? This is Slashdot.

You forgot to finish with the kick into the pit of death.

Oh, so that's what Beta is for (4, Funny)

Tenebrousedge (1226584) | about 7 months ago | (#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?

Very fi (1)

Impy the Impiuos Imp (442658) | about 7 months ago | (#46278505)

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.

prove that the program works (1)

Khashishi (775369) | about 7 months ago | (#46278533)

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

Re:prove that the program works (1)

cdrudge (68377) | about 7 months ago | (#46278643)

Run the program a few times, so the probability of errors in the output is close to zero.

No. If it's indeed a proof the probability of errors must be 0, not just close to it.

Re:prove that the program works (1)

tepples (727027) | about 7 months ago | (#46279023)

First prove, with a zero probability of errors, that the world you live in is the real world as opposed to a simulation performing a Sybil attack through all five senses.

Re:prove that the program works (2)

sexconker (1179573) | about 7 months ago | (#46279173)

Run the program a few times, so the probability of errors in the output is close to zero.

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.

Re:prove that the program works (1)

lgw (121541) | about 7 months ago | (#46279365)

There's not really any such thing as "provably correct logic" to begin with. A some point you just have to decide that the chance of errors across the process is low enough to go on with. I think of this as the "certainty noise floor": it's not important whether the chance of error is 0, but that the chance is really quite small, because that's the best we ever get.

Re:prove that the program works (1)

Your.Master (1088569) | about 7 months ago | (#46279191)

Re-running the program is equivalent to having more than one mathematician review the proof. In both cases, you're trying to drive the probability of error in verification down to zero.

Re:prove that the program works (0)

Anonymous Coward | about 7 months ago | (#46278651)

That's not maths. We don't accept "the probability of this being wrong is close to zero" as proof - proof has to be absolute. So the only way that you could get this past a real mathematician would be to run the computer program an infinite number of times and find that at that limit the probability you were wrong was exactly zero. Maths doesn't submit to the scientific method. Mathematical proof is done through logic (induction, reducto ad absurdum etc) not experiment.

Re:prove that the program works (0)

Anonymous Coward | about 7 months ago | (#46278903)

The poster is not suggesting experimentation.

Consider using a computer to prove that 2+2 = 4
It could be done in the following way.
1) Add 2 + 2
2) Check if the result is 4
Will this procedure work? Normally, yes. If you research some of the terms in the post you replied too, you’ll learn that sometimes outside influences cause digital circuits to output wrong results. As transistor sizes has decreased the danger of such things have increased and so has the research in preventing them. Looks like the poster is concerned enough with such a possibility as to want the calculation repeated to guard against the result being caused by a single event upset or similar.

Re:prove that the program works (2)

weilawei (897823) | about 7 months ago | (#46279127)

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.

Re:prove that the program works (1)

lgw (121541) | about 7 months ago | (#46279393)

Proof is absolute, within the confines of the accepted axioms.

No, not really. Or perhaps I should say: one can never be absolutely certain that a proof is correct. Practically the flaws in the model (when the model is just math) are so small compared to likely flaws in the modeling that it's best to ignore them, but even in the abstract there is no "absolute proof".

that word does not mean what you think it means (1)

SlashDread (38969) | about 7 months ago | (#46278687)

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

Re:that word does not mean what you think it means (1)

careysub (976506) | about 7 months ago | (#46279117)

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

This isn't a probabilistic 'proof' - it is straight-up deterministic: the SAT result proves it true. Period.

The poster above is alluding to the fact that a random software error could occur that gives the same result erroneously. Thus running the program is used to show that this isn't the case at all.

To assert that a lengthy, complex mathematical proof entirely written by a human is absolutely true requires you to believe the human is incapable of error (Wile's proof of the FLT ran 150 pages and this is not exceptional). The probability that a proof-author and a few successive reviewers could miss a mistake is astronomically greater than the chance of multiple random computer error corrupting the SAT calculation.

Re:prove that the program works (1)

ThanatosMinor (1046978) | about 7 months ago | (#46278715)

Prove that the algorithm works. That's your proof.

Gödel [wikipedia.org] and Turing [wikipedia.org] 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.

Re:prove that the program works (1)

ThanatosMinor (1046978) | about 7 months ago | (#46278763)

Forgot to mention those guys showed that such an algorithm that "works" for all valid proofs is not just difficult but mathematically impossible.

Re:prove that the program works (1)

Anonymous Coward | about 7 months ago | (#46278803)

If you prove the algorithm works, you prove it for all inputs.

Re:prove that the program works (5, Informative)

ClickOnThis (137803) | about 7 months ago | (#46278865)

Prove that the algorithm works. That's your proof.

Gödel [wikipedia.org] and Turing [wikipedia.org] 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.

Re:prove that the program works (1)

weilawei (897823) | about 7 months ago | (#46279175)

If the algorithm can be proved correct (within whatever axiomatic system you're using) then it's correct. The End.

Thank you. For the love of FSM, thank you for qualifying your statement about proof.

Re:prove that the program works (1)

ThanatosMinor (1046978) | about 7 months ago | (#46279183)

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.

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

Sure, if errors are found in a generating algorithm, then they will be fixed and it will be run again, but that again doesn't show that its "proof" is a real proof without independent verification, which again invokes the halting problem if its proof is horrendously long since what it creates must be evaluated by another algorithm. There is no way to demonstrate that such an algorithm as this generates only correct proofs.

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.

Considering how complex computer systems are, is it even possible to claim that an algorithm can run bug-free enough to consider correctness of code equivalent to verification that its output is correct in any but trivial cases?

Re:prove that the program works (3, Insightful)

ClickOnThis (137803) | about 7 months ago | (#46279673)

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.

Re:prove that the program works (1)

ThanatosMinor (1046978) | about 7 months ago | (#46279347)

Note also the poster I responded to didn't say prove the algorithm is correct and error-free, but rather that it "works," which means generates a correct proof, the checking of which (probably) invokes the halting problem. I say probably because it's likely no easier to write an algorithm that is designed specifically to check this "proof" for correctness than it is for a mathematician to verify it manually, and therefore it would be verified by a general one designed to verify proofs. The halting problem doesn't apply to the former case since it would involve a single-use algorithm to verify one single input, but it surely applies to the latter.

Re:prove that the program works (0)

Anonymous Coward | about 7 months ago | (#46278807)

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.

True dat!

Human Mathematician

Re: (-1)

Anonymous Coward | about 7 months ago | (#46278587)

Here's another mathematical proof that takes less space than the entirety of Wikipedia:
Fuck Beta

Stay away from SAT solvers (1)

Anonymous Coward | about 7 months ago | (#46278839)

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.

Conclusion is good (1)

gweihir (88907) | about 7 months ago | (#46278863)

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.

Re:Conclusion is good (0)

Anonymous Coward | about 7 months ago | (#46279643)

Agreed, the interesting thing here is that he showed that there isn't a solution for a given number: 1161. If anyone cares to show him wrong, they just need to try everything on that number and see that nothing works.

And After Politicians Use the End Result... (-1, Flamebait)

BoRegardless (721219) | about 7 months ago | (#46278893)

The danger comes when a computer is used to verify an otherwise unprovable program to give answers that justify some politicians deciding that we must "change the world to avoid disaster based on the computer analysis".

I think I read that wrong (0)

Anonymous Coward | about 7 months ago | (#46278919)

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

Need a computer to check the proof (1)

Megahard (1053072) | about 7 months ago | (#46278981)

And yes, it's computer proofs all the way down.

Canadian Prime Minister would say... (4, Funny)

jayveekay (735967) | about 7 months ago | (#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

Re:In response to the PM (2)

steelfood (895457) | about 7 months ago | (#46279223)

"Yes, I have smoked crack cocaine."

Robert Ford, mayor of Toronto.

Re:Canadian Prime Minister would say... (1)

weilawei (897823) | about 7 months ago | (#46279229)

"A poof is a poof. What kind of a poof? It's a poof. A poof is a poof. And when you have a good poof, it's because it's poofin'." Jean B. Tokin, former Prime Minister of CanIHitThat

Oh wait nevermind (1)

LordLimecat (1103839) | about 7 months ago | (#46279007)

Turns out its just a memory dump from when a processor bug caused a kernel panic.

Technological Singularity (1)

peon_a-z,A-Z,0-9$_+! (2743031) | about 7 months ago | (#46279029)

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.

Ironic (0)

Anonymous Coward | about 7 months ago | (#46279165)

The bottom /. quote for me reads as follows -

"Everything should be made as simple as possible, but not simpler." -- Albert Einstein

wait for theorem generating software (0)

Anonymous Coward | about 7 months ago | (#46279361)

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.

Proof? (0)

Anonymous Coward | about 7 months ago | (#46279481)

Human
Math hypothesis
Computer
??
??
??
??
Proof!
?
?
?
Profit!!!!

It's ONLY 6.5M pages! (0)

Anonymous Coward | about 7 months ago | (#46279501)

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:

Crowdsource the proof checking! (0)

Anonymous Coward | about 7 months ago | (#46279519)

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 (1)

canadiannomad (1745008) | about 7 months ago | (#46279587)

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.

Gonna check it out (0)

Anonymous Coward | about 7 months ago | (#46279635)

Be right back.

Load More Comments
Slashdot Login

Need an Account?

Forgot your password?

Submission Text Formatting Tips

We support a small subset of HTML, namely these tags:

  • b
  • i
  • p
  • br
  • a
  • ol
  • ul
  • li
  • dl
  • dt
  • dd
  • em
  • strong
  • tt
  • blockquote
  • div
  • quote
  • ecode

"ecode" can be used for code snippets, for example:

<ecode>    while(1) { do_something(); } </ecode>