Worked solution: Tao's proof of the Erdős discrepancy problem via logarithmically averaged correlations (2015)

For a function $f:\mathbb{N}\to\{-1,+1\}$, define its discrepancy as $\sup_{n,d\in\mathbb{N}}\left|\sum_{j=1}^n f(jd)\right|$, the largest possible absolute value of a partial sum of $f$ restricted to a homogeneous arithmetic progression $d,2d,\ldots,nd$. Paul Erdős conjectured in the 1930s that this discrepancy is always infinite, i.e. for every $f$ and every constant $C$, some $n,d$ make $\left|\sum_{j=1}^n f(jd)\right| > C$.

The problem resisted proof for over 80 years and became the subject of the 2010 Polymath5 collaborative project (initiated by Timothy Gowers), which established several partial results and equivalent reformulations but not the full conjecture. Terence Tao proved the full result in 2015 (published in Discrete Analysis, 2016), and in fact for the more general vector-valued statement where $f$ takes values in the unit sphere of any real or complex Hilbert space, not just $\{-1,+1\}$.

The rest of this proof follows Tao's three-part strategy stated in his paper's abstract: a Fourier-analytic reduction (from the Polymath5 project) to completely multiplicative functions, a logarithmically averaged form of the Elliott conjecture on correlations (Tao's own separate 2015 result), and a final argument (extending an idea also from Polymath5) that rules out the one remaining case.