# Computer-Aided Proof of Erdos Discrepancy Properties

arXiv: https://arxiv.org/abs/1405.3097 · HTML: https://mlsanity.com/paper/1405.3097/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 May 2014.

## Built on by (most cited first, 1 of 1)

- [Inverting Cryptographic Hash Functions via Cube-and-Conquer](https://mlsanity.com/paper/2212.02405/) (2022)

## Abstract (arXiv)

In 1930s Paul Erdos conjectured that for any positive integer C in any infinite ± 1 sequence (xn) there exists a subsequence xd, x2d, x3d,dots, xkd, for some positive integers k and d, such that mid sumi=1k xi· d mid >C. The conjecture has been referred to as one of the major open problems in combinatorial number theory and discrepancy theory. For the particular case of C=1 a human proof of the conjecture exists; for C=2 a bespoke computer program had generated sequences of length 1124 of discrepancy 2, but the status of the conjecture remained open even for such a small bound. We show that by encoding the problem into Boolean satisfiability and applying the state of the art SAT solvers, one can obtain a discrepancy 2 sequence of length 1160 and a proof of the ErdHos discrepancy conjecture for C=2, claiming that no discrepancy 2 sequence of length 1161, or more, exists. In the similar way, we obtain a precise bound of 127,645 on the maximal lengths of both multiplicative and completely multiplicative sequences of discrepancy 3. We also demonstrate that unrestricted discrepancy 3 sequences can be longer than 130,000.