## Submission + - A Mathematical Proof Too Long To Check (i-programmer.info)

mikejuk writes:

*We have surely got over the shock of computers being involved in mathematical proofs?*

It seems not, but in this case the proof occupies a 13GByte file — bigger than the whole of Wikipedia, so perhaps we have crossed a line.

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 find 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, is 13GBytes.

As the authors of the paper (http://arxiv.org/abs/1402.2184) write:

"[it]...is probably one of longest proofs of a non-trivial mathematical result ever produced. Its gigantic size is comparable, for example, with the size of the whole Wikipedia, so 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.It seems not, but in this case the proof occupies a 13GByte file — bigger than the whole of Wikipedia, so perhaps we have crossed a line.

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 find 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, is 13GBytes.

As the authors of the paper (http://arxiv.org/abs/1402.2184) write:

"[it]...is probably one of longest proofs of a non-trivial mathematical result ever produced. Its gigantic size is comparable, for example, with the size of the whole Wikipedia, so 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.

## A Mathematical Proof Too Long To Check More Login

## A Mathematical Proof Too Long To Check