---

Claim. For the Rademacher random multiplicative function $f$ of Problem 520, supported on the squarefree integers, and every $\eta>0$, almost surely $M_f(N)=\sum_{m\le N}f(m)\ll_{\omega,\eta}\sqrt N(\log\log N)^{1/4+\eta}$. Taking $\eta=1/8$, the ratio $M_f(N)/\sqrt{N\log\log N}$ tends to $0$ almost surely, so the limit superior the problem asks about is $0$ rather than a positive constant; the answer is no. The result is stated and proved in a Lean development, tagged v1.1.0 and pinned above to that tag's commit, with a short note in its paper/ folder; the claimant describes the development as self-contained, proving within it Harper's low-moment estimate, the prime number theorem input and the Brun–Titchmarsh inequality, and states that the proofs were largely drafted by GPT 5.6 Sol Pro and Fable 5 under their direction. The route is the same modification of Caich's argument (card) as in the two other claims: a conditional high-moment estimate on each thin block of primes, from Doob's inequality and hypercontractivity, replaces the first-moment bound and union bound that cost Caich the exponent $3/4+\varepsilon$. The claim was registered on the site's proof-claims page on 2026-08-04 by Sigurd William Rachlew Høystad, who presents the development as answering the problem in the negative, with a hedge, and credits the same bound to Durkan and Pearce-Crump (their claim page) and to the forum announcement by Korsky and Reis (the Korsky claim).

Submission note. Posted to erdosproblems.com as a proof claim by Sigurd William Rachlew Høystad (account Saasom) on 4 August 2026, giving "GPT 5.6 Sol Pro, Fable 5" as the AI used:

The Lean development linked below appears to answer Problem #520 in the negative. It proves, for the squarefree Rademacher random multiplicative function and every η > 0, that almost surely |M_f(N)| ≪_{ω,η} √N (log log N)^(1/4+η); taking η = 1/8, the ratio M_f(N)/√(N log log N) tends to 0 almost surely, so the limsup in the problem is 0 rather than a positive constant. This is the same bound recently proved by Durkan and Pearce-Crump (arXiv:2607.29429) and announced on this site by Korsky and Reis, via essentially the same modification of Caich's argument: a conditional high-moment estimate on each thin prime block, using Doob's inequality and hypercontractivity, in place of a first-moment bound and union bound. The development is self-contained: Harper's low-moment estimate, the prime number theorem input, and Brun–Titchmarsh are proved within it. The proofs were largely drafted by AI (GPT 5.6 pro / Fable 5) under my direction.

Formalization. The development is the first formalization link, pinned to the v1.1.0 tag's commit, which is written for Lean 4.30.0-rc2. The second is src/latest/ErdosProblems/Erdos520.lean in Boris Alexeev's repository plby/lean-proofs, pinned to its commit of 2026-09-15, a 35-line file whose header declares it a formalization by Høystad with GPT-5.6 Pro and Claude Fable 5 from that tag and revision. It imports the development's unconditional module, ported in that repository to Lean v4.33.0, and states two theorems: normalized_tendsto_zero, that almost surely $|M_f(N)|/\sqrt{N\log\log N}\to0$, and not_erdos_520, that no constant $c>0$ is almost surely the limit superior of $M_f(N)/\sqrt{N\log\log N}$. Their model is exactly the problem's: independent fair signs $f(p)=\pm1$, $f(n)$ the product of the signs of the prime factors of a squarefree $n$ and $0$ for every other $n$, and $M_f(N)=f(1)+\dots+f(N)$, normalized by $\sqrt{N\log\log N}$. The formal-conjectures statement of the problem quantifies over every family satisfying its IsRademacherMultiplicative predicate, and the catalog's change records a separately compiled bridge from the development's model to that statement, which the file does not contain; the bridge matters only for the catalog's statement over all such models, not for the question above. The catalog's formal_proof attribute names this file (the pinned link to the statement file is on the problem page). It declares itself a formalization of this claim, so it is recorded here and gets no page of its own.

Depends on. Nothing in this wiki.

Acceptance. Formalized. This corpus's verification built plby/lean-proofs at the pinned commit of 2026-09-15 (Lean v4.33.0, Mathlib v4.33.0; the module ErdosProblems.Erdos520 and the development it imports) and checked the axioms of Erdos.Problem520.not_erdos_520 and Erdos.Problem520.normalized_tendsto_zero, which are exactly propext, Classical.choice and Quot.sound; a text search of the development's tree found no sorry, axiom or native_decide. What was built is that repository's port of the v1.1.0 development to Lean v4.33.0, not the tagged payload itself. The repository's comparator challenge ComparatorChallenges/ErdosProblems/Erdos520.lean pins both theorems with the definitions their types reach (the sample space of sign sequences, the fair coin, its infinite product measure, the signs, $f$ and the partial sums), and the fingerprints of both theorems were found identical to the challenge; the solution's definitions and statements are textually identical to the challenge's. The statement was audited clause by clause against the problem's Statement: the signs are fair independent coins, and the infinite product is the genuine product measure because each coin has mass $1$; $f(1)=1$, and $f$ is the product over prime factors on squarefree $n$ and $0$ otherwise; $M_f(N)=f(1)+\dots+f(N)$; the denominator takes a junk value only for $N\le2$, which no limit sees; and since the only junk value of Lean's real limit superior is $0$, an almost sure limit superior equal to some $c>0$ holds in Lean exactly when it holds for the true limit superior. So not_erdos_520 is exactly the answer no, and normalized_tendsto_zero gives the limit superior $0$. The formalized evidence covers only these two compared theorems, no positive constant and the ratio tending to $0$; it does not cover the almost sure bound $M_f(N)\ll\sqrt N(\log\log N)^{1/4+\eta}$, which is the development's criticalUpperBound_unconditional, not a compared theorem. Not reviewed: the site labels the problem OPEN and listed the claim with no comments and the formal-conjectures catalog, which tagged its statement research solved on 2026-09-18 crediting Høystad 2026, links the proof without refereeing it. Not refereed: the claim is a forum posting with a short note, and no refereed version was found.