---

Claim. The answer to Problem 1150 is no: no constant $c>0$ makes every $\pm1$ polynomial of every large degree $n$ exceed $(1+c)\sqrt n$ in maximum modulus on the unit circle. Write $m_N$ for the minimum, over signs $\varepsilon_0,\ldots,\varepsilon_{N-1}\in\{-1,1\}$, of $N^{-1/2}\max_{\lvert z\rvert=1}\lvert\sum_{k<N}\varepsilon_kz^k\rvert$; Parseval's identity gives $m_N\ge1$. Theorem 1.1 of OpenAI, Asymptotically minimal maxima of real Littlewood polynomials, OpenAI Math Release preprint, 23 September 2026, at the pinned revision of the release repository (the preprint link), states that $m_N\to1$: for every $\eta>0$ there is $N_0$ such that every integer $N\ge N_0$ admits signs $\varepsilon_0,\ldots,\varepsilon_{N-1}$ with

$$\max_{\lvert z\rvert=1}\Bigl\lvert\sum_{k=0}^{N-1}\varepsilon_kz^k\Bigr\rvert \le(1+\eta)\sqrt N .$$

The manuscript is paged at the result page of its card. The bridge to the Statement is elementary: a sum of $N$ terms with coefficients $\pm1$ is a polynomial of degree $n=N-1$ with coefficients $\pm1$. Given $c>0$ take $\eta=c/2$ and $N_1\ge N_0$ so large that $(1+c/2)\sqrt N\le(1+c)\sqrt{N-1}$ for every $N\ge N_1$; then for every degree $n\ge N_1-1$ the theorem's polynomial of length $n+1$ has maximum modulus at most $(1+c)\sqrt n$, so the inequality of the Statement fails for every large $n$, not merely for some. The theorem is one-sided and existential: the manuscript's remark after Theorem 1.1 says that it gives no lower bound for $\lvert P\rvert$ on the circle, the release's family document says that it gives no convergence rate and no signing algorithm, and the manuscript notes that the additive gap $\max\lvert P\rvert^2\ge N+(N-1)^{1/3}/38$ of Erdélyi 2026 (card erdelyi_2026_erdos_problem_about_maximum_modulus_littlewood_polynomials_unit_circl) is compatible with it, that excess being $o(N)$. The proof first builds relaxed coefficients in $[-1,1]$ with small defect from signs by sampling quadratic-phase waves off a real trigonometric polynomial on an auxiliary torus, packing their Fourier supports with the Pippenger–Spencer coloring theorem, then rounds them to signs with a defect-sensitive discrepancy bound in the partial-coloring method of Spencer and Lovett and Meka (Sections 2–6). The same manuscript derives unbounded binary merit factors through all lengths, a uniquely ergodic binary Morse shift with simple spectrum whose zero-coordinate spectral measure is absolutely continuous ($L^2$ density), and $L^p$ flatness for every finite $p$, and its Appendix A disputes nonflatness claims in preprints of el Abdalaoui (el Abdalaoui's three claims of an answer to this problem have rejected pages: 2016, April 2025 and September 2025); none of these is part of this claim. Two later release manuscripts of 5 October 2026 strengthen the construction without Lean: Nearly minimal maxima and positive minima of Littlewood polynomials (Theorem 1.1 of its card) adds the lower bound $\sqrt N/16\le\lvert P(z)\rvert$ to the same upper bound, and Ultraflat real Littlewood polynomials (Theorem 1 of its card) states that for every $\varepsilon\in(0,1)$ and every large $N$ some signs give $(1-\varepsilon)\sqrt N\le\lvert P(z)\rvert\le(1+\varepsilon)\sqrt N$ on the whole circle, $z=\pm1$ included, which is the two-sided ultraflat polynomial the site's commentary names. Each contains the upper bound and so the answer no, but their two-sided statements are claimed, not accepted, and are recorded on the pending claim page of Problem 228; their links on this page are provenance for the stronger claims and contribute no evidence. The same theorem is a second disproof of Problem 230, recorded on that problem's claim page.

Depends on. Nothing in this wiki: the proof is self-contained in the manuscript and its Lean tree, and the Lean statement rests on Mathlib's finite sums, complex norm and Real.sqrt alone.

Acceptance. A disproof of Problem 1150; its Lean declaration was built by this corpus's verification with the three standard axioms and its statement audited for fidelity. Formalized: the declaration OAI.AsymptoticallyMinimalLittlewood.main of the release's lean/ folder (file OAI/Analysis/Littlewood/Main.lean, with MainStatement, littlewoodValue and IsRealSigning in Model.lean) proves exactly the display above: for every real $\eta>0$ there is $N_0\ge1$ such that for every $N\ge N_0$ some $\varepsilon:\mathrm{Fin}\,N\to\mathbb R$ with every value $-1$ or $1$ has $\lVert\sum_k\varepsilon_kz^k\rVert\le(1+\eta)\sqrt N$ for every complex $z$ of norm $1$. This corpus's verification built the solution module and the comparator challenge ComparatorChallenges/AsymptoticallyMinimalLittlewood.lean, which pins the declaration, from the release at the pinned revision, printed the declaration's axioms, which were exactly propext, Classical.choice and Quot.sound, and found the comparator fingerprint of the pinned challenge statement identical to the solution's; the result was recorded on 2026-10-07. The statement audit that formalized requires is this corpus's own: a statement-fidelity audit unfolded littlewoodValue and IsRealSigning, checked the quantifiers and the coercions (the natural $N$ to a real under the square root, the real signs to complex coefficients, Fin indices to exponents) for junk values and found none, compared the declaration with the problem page's Statement (the coefficient class, the degree $N-1$ against the Statement's $n$, the circle, the bound and the quantifiers over $c$ and $n$) and with the formal-conjectures statement erdos_1150 (https://github.com/google-deepmind/formal-conjectures/blob/6fbb54f24ccc2e64dcfaffc28c58950e377110d2/FormalConjectures/ErdosProblems/1150.lean): its eventual range in $n$, its coefficient class fixed by the natural degree, and its supremum over the circle against the declaration's pointwise bound; it noted that the bound is not trivial since for small $\eta$ it beats the Rudin–Shapiro polynomials, and judged that the declaration refutes the question through the bridge above. The release's family document says the results are existential, with no effective rate and no signing algorithm. Not reviewed: no outside reviewer or independent acceptance of the result is recorded; the site's label is OPEN with an empty proof-claims tab. Not refereed: the manuscripts are unrefereed release preprints with no arXiv version. The release's own README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification. Only the pinned revision is described; later revisions are unexamined.