A published paper or arXiv preprint answers the main question of Erdős Problem #520 (theorem erdos_520 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

The problem, as stated in formal-conjectures (Apache 2.0):

Let f be a Rademacher multiplicative function. Does there exist some constant c > 0 such that, almost surely, \limsup_{N \to \infty} \frac{\sum_{m \leq N} f(m)}{\sqrt{N \log \log N}} = c? The answer is no: Høystad [Hø26] (with GPT-5.6 Pro and Claude) proved, following the Halász–Lau–Tenenbaum–Wu–Caich martingale approach with Harper's low-moment estimates [Ha13], that almost surely \sum_{m \le N} f(m) \ll \sqrt{N} (\log \log N)^{1/4 + \eta} for every \eta > 0, so the \limsup is 0 almost surely. The linked formal proof works with the concrete model `ℕ → Bool` with the product of fair coins, whose squarefree-supported Rademacher function is `IsRademacherMultiplicative`; this refutes the statement below.

References formal-conjectures lists for this problem (a starting point, not evidence):

• [Hø26] Høystad, S. W. R., A self-contained Lean 4 proof that Erdős Problem #520 has a negative answer (2026),
• [Ha13] Harper, A. J., Bounds on the suprema of Gaussian processes, and omega results for the sum of a random multiplicative function. Ann. Appl. Probab. 23 (2013), 584–616.