Computer-Aided Proof of Erdos Discrepancy Properties

TL;DR

This paper uses advanced SAT solvers to prove bounds on the length of sequences with certain discrepancy properties, resolving Erdős's conjecture for discrepancy 2 and providing new bounds for discrepancy 3.

Contribution

It introduces a novel computational approach encoding discrepancy problems into SAT, achieving the first proof of Erdős's conjecture for discrepancy 2 and establishing new sequence length bounds.

Findings

Discrepancy 2 sequences of length 1160 exist, but none longer than 1160.

Maximum length of multiplicative sequences with discrepancy 3 is 127,645.

Unrestricted discrepancy 3 sequences can exceed 130,000 in length.

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\H{o}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 $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$.