Computer-Aided Proof of Erdos Discrepancy Properties

Abstract

In 1930s Paul Erdos conjectured that for any positive integer $C$ in any infinite $\pm 1$ sequence $(x_n)$ there exists a subsequence $x_d,x_{2d},x_{3d},\dots ,x_{kd}$, for some positive integers $k$ and $d$, such that $\mid {\sum }_{i=1}^k{x}_{i\cdot 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 Erdős 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 $127645$ 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 $130000$.

Revised and extended journal version of arXiv:1402.2184, http://arxiv.org/abs/1402.2184