## A Mathematical Proof Too Long To Check 189

Posted
by
Soulskill

from the which-this-margin-is-too-narrow-to-contain dept.

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."*
## Re:To long, didn't check. (Score:5, Informative)

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

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:the beginning, not the end (Score:2, Informative)

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

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

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

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.