Forgot your password?
typodupeerror
Math

A Mathematical Proof Too Long To Check 189

Posted by Soulskill
from the which-this-margin-is-too-narrow-to-contain dept.
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."
This discussion has been archived. No new comments can be posted.

A Mathematical Proof Too Long To Check

Comments Filter:
  • by Garridan (597129) on Tuesday February 18, 2014 @02:11PM (#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.
  • by ClickOnThis (137803) on Tuesday February 18, 2014 @02:36PM (#46278865) Journal

    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.

  • by Anonymous Coward on Tuesday February 18, 2014 @02:45PM (#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.
  • by K. S. Kyosuke (729550) on Tuesday February 18, 2014 @03:04PM (#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.
  • by Mask (87752) on Tuesday February 18, 2014 @04:03PM (#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.

  • by firewrought (36952) on Tuesday February 18, 2014 @05:30PM (#46280393)

    But you'd have to be an idiot to want to check this proof without a computer.

    Historically, mathematicians have resisted computer-only proofs. They want eyeballs end-to-end. Your ideas (independent implementations, hardware, etc.) are sound/feasible from a software engineering standpoint, but unsatisfying to mathematicians. (Not being a mathematician myself, I'm ill-suited to testify as to why that's the case, but so it is.)

    Maybe one day that mindset will be abandoned, but what's more likely to happen is that mathematics will bifurcate: there will be the set of mathematics that relies on computer proofs and the "pure" subset of that that doesn't require computers. Probably, that's already considered the case. Regardless, this is how the field has dealt with countless other issues (such as not accepting negative proofs [wikipedia.org]), often to great fecundity.

Between infinite and short there is a big difference. -- G.H. Gonnet

Working...