---

Ethan Yang, A bounded counterexample for lacunary averages with endpoint Fourier decay, dated 26 September 2026 and published in the author's repository erdos-996-lean, gives a second negative answer. Theorem 1.1 constructs a measurable $f\colon\mathbb T\to\{0,1\}$ and a strictly increasing sequence of positive integers with $n_{j+1}\ge 2n_j$ such that $\int f\,d\mu\le 1/16$, $\|f-S_mf\|_2\le 8/\sqrt{\log\log m}$ for all sufficiently large $m$, and $\limsup_N N^{-1}\sum_{j\le N}f(n_jx)\ge 3/4$ for almost every $x$. Corollary 1.2 concludes that no absolute $C>0$ makes the condition $\|f-S_mf\|_2=O((\log\log\log m)^{-C})$ sufficient, the same function and sequence working for every fixed $C$. The function is the indicator of a union of rare binary-word events; a rarer subevent forces a long run of ones under the doubling map, the sampling sequence consists of blocks of consecutive powers of two separated so that the favorable events are independent, each block has three times as many terms as all earlier ones, the second Borel-Cantelli lemma gives infinitely many successful blocks, and finite binary approximations control the Fourier tail. The paper states that it claims no priority: Ho's Theorem 1.1 and Corollary 1.4 gave the negative answer with an unbounded function of infinite limit superior at the same decay exponent, and Ho's Theorem 1.7 gave a bounded construction without a Fourier-tail estimate; the new point is a bounded observable with the endpoint decay. The statements are those of the PDF at the pinned revision; the proofs were not checked here. The earlier disproof is Ho's page.

Submission note. Posted to erdosproblems.com as a proof claim by Ethan Yang (account EthanYang) on 26 September 2026, giving "GPT-6 Astra, GPT-5.6 Sol" as the AI used:

I give an alternative disproof of Erdős Problem #996 using a bounded indicator function. The construction gives f taking values in {0,1} and integers n_{j+1} >= 2n_j such that ||f-S_m f||_2 <= 8/sqrt(log log m) for all sufficiently large m, while integral f <= 1/16 and the sampled averages have limsup at least 3/4 almost everywhere. The same pair satisfies every fixed positive triple-logarithmic exponent, so no absolute C in the question exists. The construction uses a rare binary word whose occurrence persists through many shifts. Trials using disjoint digit windows are independent, and each successful trial forces a block of ones large enough to dominate the preceding observations. Borel–Cantelli gives infinitely many successes. Finite binary approximations and an elementary step-function Fourier estimate control the tail at every sufficiently large cutoff. Notes: Boon Suan Ho previously gave a disproof in arXiv:2604.18535v2. This is an alternative construction, not a claim of priority for the original resolution. The paper compares the constructions. GPT-6 Astra generated the mathematical proof and was used for statement reconstruction, review, and writing. GPT-5.6 Sol was used for the Lean implementation. The Lean 4/Mathlib development is complete and unconditional. It reproduces the positive statement from Google DeepMind's Formal Conjectures project and independently proves its negation; it does not import the unresolved theorem or its answer(sorry) wrapper. DeepMind supplied the reference statement, not this proof. The final theorems have no undischarged hypotheses or sorryAx; their axiom reports contain exactly propext, Classical.choice, and Quot.sound. No independent human expert review is claimed. I welcome checking of the statement correspondence and exposition.

Standing. The result was filed on the site's proof-claims tab on 26 September 2026; the tab names GPT-6 Astra and GPT-5.6 Sol, and the claim's notes say that GPT-6 Astra generated the proof and was used for statement reconstruction, review and writing, and that GPT-5.6 Sol was used for the Lean implementation. The two thread comments of 27 September 2026 ask whether Ho's Theorem 1.1 is stronger, and the author answers that it gives the stronger divergence conclusion at the same rate while the present function takes only the values $0$ and $1$. The site's label is unchanged (OPEN), no human review is claimed and none is named, and the write-up is not refereed, so the claim stays claimed.

Formalization. The repository's Lean 4 development states the theorem as Erdos996.erdos996_main and proves Erdos996.erdos996_answer : False ↔ Erdos996.SourceStatement, where the source statement reproduces the formal-conjectures statement of the problem rather than importing it; the README reports that the final theorems depend only on the axioms propext, Classical.choice and Quot.sound and contain no sorry. The formal-conjectures statement file, at its revision of 18 September 2026, tags the problem research open and carries no formal_proof attribute. The corpus has built and audited nothing, so the claim lists no formalized evidence.