Claim. For every sequence $x_1,x_2,\ldots\in(0,1)$, $\limsup_{k\to\infty}A_k=\infty$ with $A_k=\limsup_n\lvert\sum_{j\le n}e(kx_j)\rvert$. This is the qualitative part of Clunie's theorem, which gives the rate $k^{1/2}$. Of the two proofs of 2025-08-30, the first is qualitative and the second was introduced by Tao as an alternate, more quantitative proof that avoids the compactness step; both were posted before the thread found the earlier literature. Tao's comment of 2025-08-31 reports that Erdős himself had solved the first question shortly after posing it, with the logarithmic bound recorded on Erdős's claim page, and that Clunie had raised it to $k^{1/2}$; its closing edit adds that Tao's technique recovers Clunie's $k^{1/2}$ bound, as the site's commentary records. The formalized statement is the qualitative form.

Covers. The first question of Problem 987. The second question is answered by the 2026 construction.

Depends on. Nothing in this wiki; the argument is self-contained, and Clunie's theorem is the earlier, quantitative answer to the same question.

Arguments. The thread of 2025-08-30 carries two proofs. The first assumes the limit superior is finite, passes to a subsequence by weak compactness and averages to a contradiction. The second avoids compactness: a double Fourier series computation bounds the sum over $j,j'\le n$ of $\lvert\sum_{k<K}(z_j/z_{j'})^k\rvert^2$ from below by $nK^2$ and from above by a quantity that forces the sums to be large for some $k<K$.

Formalization. The Lean 4 file erdos_987.lean in the author's analysis repository, added on 2025-08-30, states

theorem Erdos_987 (z : ℕ → Circle) :
  atTop.limsup (fun k : ℕ ↦ atTop.limsup (fun n : ℕ ↦
    (‖∑ j ∈ range n, ((z j)^k : ℂ)‖ : EReal))) = ⊤

with $z_j=e(x_j)$ on the unit circle and indices from $0$. Not audited here: the statement allows every point of the circle, so it covers the problem's sequences in $(0,1)$, and it is the second proof formalized against Mathlib. The pinned commit (2025-08-30 22:57 UTC) is the author's last change of that day; later commits of March 2026 track toolchain and literate-programming changes. The second formalization link is the contributor's fork of formal-conjectures whose erdos_987.parts.i proves the first question by an argument its comments say is adapted from this file, over sequences in $(0,1)$; the repository's main branch points its formal_proof attributes at that fork. The community database's Lean status, dated 2026-08-23, came seven weeks after those attributes were merged into main on 2 July 2026, in Boris Alexeev's batch of forty problems whose solutions the lean-proofs collection formalizes. Boris Alexeev's lean-proofs file Erdos987.lean, linked above, proves erdos_987 by the same second proof adapted from this file; it is described on the Alexeev et al. claim page. None of these files was built or audited here, so this corpus assigns no formalized evidence.

Acceptance. Reviewed: the site's curator, Thomas Bloom, acknowledged the proof in the thread on 2025-08-30, and the site's commentary credits Tao with an independent proof of the $k^{1/2}$ bound; the theorem is the qualitative form of Clunie's refereed result. Not refereed; a forum posting.