# A Mathematical Proof Too Long To Check

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

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

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

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

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

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

toolong, didn't check." I guess I should have checked.## Re:To long, didn't check. (1)

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

Opps, "

toolong, 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 8 months ago | (#46278355)

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

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

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

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

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

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

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 8 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 8 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 8 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 8 months ago | (#46278263)

## Re:News for nerds (1)

## cheater512 (783349) | about 8 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 8 months ago | (#46278277)

less space than wikipedia? that sounds large.

wtf?

## Re:wow (5, Funny)

## HaZardman27 (1521119) | about 8 months ago | (#46278331)

## Re:wow (-1)

## Anonymous Coward | about 8 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 8 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 8 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 8 months ago | (#46278831)

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

## Re:wow (1)

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

## Re:wow (1)

## maxwell demon (590494) | about 8 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 8 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 8 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 8 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 8 months ago | (#46279071)

## Re:wow (0)

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

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

## Re:wow (1)

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

## Re:wow (3, Insightful)

## Nexus7 (2919) | about 8 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 8 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 8 months ago | (#46278283)

## the beginning, not the end (5, Interesting)

## EngineeringStudent (3003337) | about 8 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 8 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 8 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 8 months ago | (#46278453)

forloop "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 8 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 8 months ago | (#46279687)

forloop", not a bit. A modern SAT solver can solve problems with millions of variables and hundreds of thousand clauses. In contrast, a brute forceforloop 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:

SAT is clearly NP complete, and clearly the existence of good SAT solvers is

nota 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 8 months ago | (#46279817)

I'd hesitate to call one big

forloop "AI."So you would more readily accept a big ;-)

whileloop as AI?## Re:the beginning, not the end (2, Informative)

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

## Re:the beginning, not the end (1)

## DriedClexler (814907) | about 8 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 8 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 8 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 8 months ago | (#46278549)

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

## Re:After 9.5gigs (2)

## maxwell demon (590494) | about 8 months ago | (#46279849)

Actually it contains the step "then a miracle occurs." [blogspot.com]

## Paging Mr Fermat... (5, Funny)

## UdoKeir (239957) | about 8 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 8 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 8 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 8 months ago | (#46278361)

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 8 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 8 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 8 months ago | (#46279315)

"whallah"? Really?

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

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

Just saying.

## Less space than Wikipedia (5, Insightful)

## BlueMonk (101716) | about 8 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

morespace?## Re:Less space than Wikipedia (-1)

## Anonymous Coward | about 8 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 8 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 8 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 8 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 8 months ago | (#46278735)

Editor? This is Slashdot.

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

## Anonymous Coward | about 8 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 8 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 8 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 8 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 8 months ago | (#46278643)

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 8 months ago | (#46279023)

## Re:prove that the program works (2)

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

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 8 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 8 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 8 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 8 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 8 months ago | (#46279127)

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 8 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 8 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 8 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

randomsoftware 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 8 months ago | (#46278715)

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 8 months ago | (#46278763)

## Re:prove that the program works (1)

## Anonymous Coward | about 8 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 8 months ago | (#46278865)

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

truebut cannot beproved.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 8 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 8 months ago | (#46279183)

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 8 months ago | (#46279673)

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

changewhat 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

invalidproofs of the Pythagorean Theorem. But showing that a proof is invalid does not mean thetheoremis 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

limitationson the ability of algorithms to decidecertainpropositions. It doesnotmean 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

specificalgorithms to prove things because no suchuniversalalgorithm can be created.## Re:prove that the program works (1)

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

## Re:prove that the program works (0)

## Anonymous Coward | about 8 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 8 months ago | (#46278587)

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

Fuck Beta

## YUO FAIL IT (-1)

## Anonymous Coward | about 8 months ago | (#46278747)

## Stay away from SAT solvers (1)

## Anonymous Coward | about 8 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 8 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 8 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 8 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 8 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 8 months ago | (#46278981)

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

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

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

"Yes, I have smoked crack cocaine."

Robert Ford, mayor of Toronto.

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

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

## Oh wait nevermind (1)

## LordLimecat (1103839) | about 8 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 8 months ago | (#46279029)

## Ironic (0)

## Anonymous Coward | about 8 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 8 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 8 months ago | (#46279481)

Human

Math hypothesis

Computer

??

??

??

??

Proof!

?

?

?

Profit!!!!

## It's ONLY 6.5M pages! (0)

## Anonymous Coward | about 8 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 8 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 8 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 8 months ago | (#46279635)

Be right back.