---

Claim. Let $f$ be the Rademacher random multiplicative function of Problem 520 and $M_f(N)=\sum_{m\le N}f(m)$. The claim is that for every $\varepsilon>0$, almost surely $M_f(N)\ll\sqrt N(\log\log N)^{1/4+\varepsilon}$, so that Harper's conjectured exponent $1/4+o(1)$ is sharp and $M_f(N)/\sqrt{N\log\log N}\to0$ almost surely; the limit superior the problem asks about is $0$, not a positive constant, and the answer is no. The route modifies Caich's almost sure upper bound (card), whose exponent $3/4+\varepsilon$ comes from a first-moment bound and a union bound over blocks of primes: in the Rademacher model one proves instead a conditional high-moment estimate on each block, $(\mathbb E[U_j^q\mid\mathcal F_{y_{j-1}}])^{1/q}\ll_qI_{j-1}$, from Doob's $L^{2q}$ inequality, Bonami–Halász hypercontractivity, Minkowski's inequality and the fact that each block carries reciprocal-prime mass $O(1/\ell)$; a fixed large $q$ then removes the union-bound loss. The claimant registered the result on the site's proof-claims page on 2026-07-29 and states that the argument was produced by GPT 5.6-Pro with no mathematical input from them beyond the prompt, that the claimant and Victor Reis formalized part of it in Lean with five statements from Caich's paper taken as hypotheses and the key Proposition 3.1 resting on analytic tools not in Mathlib, that neither of them can verify the proof, and that the manuscript was sent to experts whose first impressions the claimant reports as favorable.

Submission note. Posted to erdosproblems.com as a proof claim by Samuel Korsky (account SamKorsky) on 29 July 2026, giving "GPT 5.6-Pro" as the AI used:

GPT 5.6 Pro claims to resolve Problem #520 in the negative, in particular Harper's conjectured $1/4 + o(1)$ exponent is sharp. In Caich’s argument, the loss from exponent $1/4+\varepsilon$ to $3/4+\varepsilon$ appears to come from applying a first-moment bound and union bound over prime blocks. For the Rademacher model, one can instead prove a conditional high-moment estimate

$$> \left(\mathbb E[U_j^q\mid\mathcal F_{y_{j-1}}]\right)^{1/q}\ll_q I_{j-1} >$$

using ordinary Doob $L^{2q}$, Bonami–Halász hypercontractivity, Minkowski,

and the fact that each prime block has reciprocal-prime mass $O(1/\ell)$. Taking fixed $q$ large enough removes the union-bound loss This work was performed with no human input at all (I just thought the contrast between Harper's conjecture and the Law of the Iterated Logarithm was surprising, so asked GPT to opine and it came up with this), although I attempted to (prompt GPT to) rewrite the proof to make it more readable. Notes: Victor Reis and I also attempted to (partially) formalize the results in Lean here: https://drive.google.com/file/d/1GAbArk0C1HFFJtrgi8bY_oicpJ5GZ-xq/view. Note that this formalization is not self-contained; we use five inputs from Caich's paper as black box hypotheses, and also the proof of Proposition 3.1 (which is the critical patch to Caich's argument) relies on some standard analytic tools not yet in Mathlib. Neither of us have the technical expertise to verify the proof ourselves; however, we have sent the manuscript to experts familiar with this problem, and initial impressions seem favorable. We wanted to post in case those more familiar with the problem found the idea interesting/plausible.

Depends on. Nothing in this wiki.

Standing. Pending: a manuscript on a file-sharing link, a formalization that is not self-contained, no referee and no acceptance by the site, which labels the problem OPEN and whose proof-claim entry carried no comments. The same bound was posted to arXiv two days later by Durkan and Pearce-Crump (their claim page) and proved again in a self-contained Lean development by Høystad (Høystad's claim page), who describes all three as essentially the same modification of Caich's argument.