---

Claim. Let $f$ be the random completely multiplicative function with $f(p)\in\{-1,1\}$ chosen independently and uniformly at each prime, and $S(N)=\sum_{m\le N}f(m)$. Then, with probability one,

$$\limsup_{N\to\infty}\frac{S(N)}{\sqrt N}=\infty .$$

This answers Problem 1144 yes. The claim was registered on the site's proof-claims page on 2026-09-06 by Sigurd William Rachlew Høystad, who credits GPT 6 Astra, GPT 5.6 Sol Pro and Fable 5, with a write-up and a Lean 4 repository, both linked above at the commit the repository's tag v1.0.0 names (tagged 2026-09-06).

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

For a completely multiplicative random function with independent fair signs at primes, the normalized partial sums have almost surely infinite positive limsup. The proof transfers squarefree Gaussian lower bounds to the complete model using stationary covariance comparisons and uniform error estimates, then applies fresh-prime Gaussian approximation. Notes: The standalone Lean build and final theorem’s axiom audit passed. The theorem depends only on Lean’s standard axioms.

Argument, as the write-up states it. The lower bound is first obtained for the auxiliary squarefree model, the Rademacher function supported on squarefree integers, through Gaussian lower bounds of the kind Harper proved for that model; it is then carried to the completely multiplicative model by comparing the covariance structures of the complete, squarefree and a stationary process (positive semidefinite decompositions, with uniform error estimates), and the final crossings above every threshold come from a Gaussian approximation driven by fresh primes, assembled into a sequence of scheduled certificates. In the claim's comments a reader asked whether the argument yields an explicit lower bound $\sup M_f(x)\gg(\log\log x)^k$ with some $k>0$ for Atherfold's weighted sums $M_f(x)=\sum_{n\le x}f(n)/\sqrt n$ (card, Theorem 3), and why such a bound would improve on Atherfold's lower bound, whose exponent is $k=-1/2$. The claimant's reply, made with the help of Astra, derives every $0<k<1/4$ from Harper's unweighted lower bound by partial summation. The other comments concern a rendering fault in an earlier copy of the write-up, which the claimant fixed the same day.

Lean development. The repository (605 modules) states the target in Targets.lean as

$$\forall^{\text{a.e.}}\omega\ \ \forall A\in\mathbb{R}\ \ \exists^{\infty}N:\ A\le\frac{S_\omega(N+1)}{\sqrt{N+1}},$$

the index shift covering every positive cutoff, and proves erdos1144 : Erdos1144 in Final.lean from a stationary candidate certificate. Its README reports that the public theorem depends only on propext, Classical.choice and Quot.sound, that an Audit.lean prints this and a GitHub Actions workflow checks it, and that historical conditional interfaces and alternative-route axioms remain in some source files and vendored blueprint tooling includes a placeholder tactic. Final.lean itself declares twelve axioms (momentConcentration, resonatorTransferCertificate and ten Harper-route certificates); by the README's axiom report, the final theorem uses none of them. The site's claim line repeats that the standalone build and the axiom audit passed. Proof coverage: none; this corpus has not built the development or printed its axioms, and no audit of the Lean target against the problem's statement is recorded, so the link is a posting of the result and not formalized evidence.

Depends on. No page of this wiki.

Acceptance. None recorded. The site's label is OPEN (problem page last edited 2026-01-26), the proof-claims entry carries six comments and no acceptance mark, the problem's discussion thread does not mention the claim, and no review, referee report or acknowledgment by anyone outside the claimant is recorded. The argument is not compiled or reviewed in this corpus.