---

Claim. For every sequence $z_1,z_2,\dots$ on the unit circle, with $M_k=\max_{\lvert z\rvert=1}\lvert\prod_{j\le k}(z-z_j)\rvert$,

$$\sum_{k\le N}M_k\gg\frac{N^{5/4}}{\sqrt{\log N}}.$$

This answers the third question of [[problems/polynomials/E0119/_index|Problem 119]] yes, with any $c<1/4$, and so settles the problem: the third question implies the second (some $k\le N$ has $M_k>N^{1/4-o(1)}$, so $M_n>n^{1/4-o(1)}$ for infinitely many $n$) and the second implies the first. The result is the proof claim registered on the site's thread on 2026-07-14 by Samuel Korsky, with GPT 5.6-Pro named there as the system used and a write-up linked from the thread; an arXiv version was announced there and none is recorded.

The argument, as the thread records it, is about a page long and uses only standard harmonic analysis. Write $z_j=e(x_j)$ and $B(x)=\log\lvert2\sin\pi x\rvert$, so that $\log M_k$ is the maximum of $B*f_k$ for $f_k$ the counting measure of $x_1,\dots,x_k$. Convolving with a Fejér kernel $K_H$ and evaluating at the next point $x_{k+1}$ bounds each $\log M_k$ from below, and summing over $k\le N$ turns the sum of these one-sided maxima into the pair sum $\sum_{i<j}(B*K_H)(x_j-x_i)$. On the Fourier side this is $\tfrac N2\log H$ up to an error of order $N+\sum_{m\le H}\lvert\widehat{f_N}(m)\rvert^2/m$. A small final maximum forces the low-frequency exponential sums to be small, $\lvert\widehat{f_N}(m)\rvert\ll m\log N$ (if $M_N$ is large, say $M_N\ge N^2$, the bound is immediate from $M_N$ alone; otherwise $\log M_N\ll\log N$ and the exponential sums are small), so with $H\asymp\sqrt N/\log N$ the average of $\log M_k$ is at least $\tfrac14\log N-\tfrac12\log\log N-O(1)$, and the arithmetic-geometric mean inequality gives the claim. The second question had been answered by a 43-page Annals paper, [[problems/polynomials/E0119/claims/1991_11_01_beck|Beck 1991]], by a much more involved analytic method; the first by Wagner 1980. A sharper bound of order $N^{3/2}$ by the same claimant is accepted on [[problems/polynomials/E0119/claims/2026_08_29_korsky|Korsky 2026 (second claim)]].

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

I plan to post an expanded and polished link to arxiv later. The claim is that for every sequence $z_j$ on the unit circle,

$$\sum_{k\le N} M_k \gg > \frac{N^{5/4}}{\sqrt{\log N}}, \qquad M_k=\max_{|z|=1}\prod_{j\le k}|z-z_j|. >$$

Writing the logarithm of the product as a sum of the kernel $B(x)=\log|2\sin

\pi x|$, one first shows that a small terminal maximum $L_t=\log M_t$ forces all low-frequency exponential sums of $x_1,\dots,x_t$ to be small. Fejér smoothing $K_H$ with parameter $H$ then bounds each prefix maximum by the interaction of the next point with the previous ones, and summing over the prefixes converts this into a pair-energy estimate. Expanding that energy in Fourier series gives a lower bound for $\sum_{k<t}L_k$, up to an error controlled by $L_t$. If $L_N$ is large, $M_N$ alone gives the result; otherwise choosing $H\asymp \sqrt N/\log N$ and applying AM–GM yields the stated bound.

Depends on. No page of this wiki: the argument is self-contained.

Acceptance. Reviewed: the site's thread marks this claim accepted by the site as correct; its curator posted a complete account of the argument on 2026-07-18, stating a belief that the proof is correct while inviting readers to check it critically, and the problem page credits the resolution of the third question to GPT 5.6 and Korsky (page last edited 2026-09-01), which the corpus counts as documented independent acceptance by the site's curator, T. F. Bloom (erdosproblems.com). The problem page's crediting sentence states the bound as $\gg n^{3/2-o(1)}$, the strength of the later claim, while the entry the thread marks accepted is this one. The community database lists the problem as solved with a Lean marker as of its last update, on 2026-08-23, which does not date the change of state. Not refereed: the write-up is a shared PDF, and no journal or arXiv version is recorded. Erdős attached a prize to this third question in [Er97f].

Formalization. Two Lean developments of this argument exist, by others, and the site's Lean marker refers to them. A forum user posted on 2026-07-17, after checking each step of the write-up, a Lean 4 development against Mathlib (the archive linked above) proving $\sum_{k\le N}M_k\ge N^{9/8}$ for all large $N$, so the third question with $c=1/8$, with the smoothing parameter $H=\lfloor N^{1/3}\rfloor$ chosen to simplify the endgame; its author states that the final theorems depend only on propext, Classical.choice and Quot.sound. The lean-proofs file linked above at its pinned commit names Codex and Boris Alexeev as formal authors and ChatGPT 5.6 Pro and Samuel Korsky as informal authors, and proves Erdos119.erdos_119 (the third question with $c=1/256$), Erdos119.erdos_119.parts.iii_quantitative (the $N^{5/4}/\sqrt{\log N}$ form) and from them parts.ii and parts.i, the second and first questions; its printed axiom lines list the three standard axioms, and the formal-conjectures statements of all three parts are marked solved with links to these declarations. Neither development has been built or audited against the question by this corpus, so the evidence lists no formalized kind; the standing rests on the site's acceptance.