Claim. 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

The manuscript is paged at the result page of its card. Real signs are coefficients of modulus one, so this refutes the constant asked for in Problem 230: given $c>0$, take $\eta=c/2$ and $n\ge\max(N_0,2)$, and put $a_k=\varepsilon_{k-1}$ for $1\le k\le n$; the site's polynomial is $z$ times the sum above, has the same modulus on the circle, and its maximum is at most $(1+c/2)\sqrt n<(1+c)\sqrt n$. The site's question was already answered no by Kahane with complex unimodular coefficients, and this is a second route with coefficients from the smaller class $\{-1,1\}$, so the same theorem answers the real-sign question of Problem 1150 negatively; that problem's page is the place for that claim. The theorem is one-sided and existential: it gives no lower bound for $\lvert P\rvert$, no convergence rate and no signing algorithm, and the manuscript notes that Erdélyi's additive gap $\max\lvert P\rvert^2\ge N+(N-1)^{1/3}/38$ is compatible with it. 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, using the partial-coloring method of Beck and Spencer in the arbitrary-vector form verified through the theorem of 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; 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, the points $z=\pm1$ included, a real-sign ultraflat family stronger than the constant-factor flatness of Problem 228. Those two statements are recorded here as the same claimant's unformalized companions; the accepted claim is Theorem 1.1 of 23 September.

Formalization. The release's Lean tree (folder lean/ at the pinned revision, with the release's pinned Lean and Mathlib) proves OAI.AsymptoticallyMinimalLittlewood.main : MainStatement in OAI/Analysis/Littlewood/Main.lean, where the comparator challenge ComparatorChallenges/AsymptoticallyMinimalLittlewood.lean defines

def littlewoodValue {N : ℕ} (ε : Fin N → ℝ) (z : ℂ) : ℂ :=
  ∑ k : Fin N, (ε k : ℂ) * z ^ (k : ℕ)

def IsRealSigning {N : ℕ} (ε : Fin N → ℝ) : Prop :=
  ∀ k, ε k = -1 ∨ ε k = 1

def MainStatement : Prop :=
  ∀ η : ℝ, 0 < η → ∃ N₀ : ℕ, 1 ≤ N₀ ∧ ∀ N : ℕ, N₀ ≤ N →
    ∃ ε : Fin N → ℝ, IsRealSigning ε ∧
      ∀ z : ℂ, ‖z‖ = 1 → ‖littlewoodValue ε z‖ ≤ (1 + η) * Real.sqrt N

and its configuration AsymptoticallyMinimalLittlewood.json pins the declaration OAI.AsymptoticallyMinimalLittlewood.main (its definition_names list is empty) and permits only the axioms propext, Quot.sound and Classical.choice; the release's catalog lean/formalization.yaml lists the declaration under this manuscript, and the release's family note pairs it with a second comparator, LittlewoodFiniteFlatness.lean, for the $L^p$ statement, which is not part of this claim. The bridge from the declaration to the site's question, the factor $z$, the passage from the pointwise bound to the maximum and the choice $\eta=c/2$ with $n\ge\max(N_0,2)$, is elementary and is not in Lean.

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 230 with real coefficients; its Lean declaration was built here with the three standard axioms and its statement audited here for fidelity. Formalized: this corpus's verification built the solution module and the comparator challenge from the release at the pinned revision, printed the axioms of the declaration, 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, compared the declaration with the problem page's Statement (the coefficient class, the index range, the circle, the bound and the quantifiers over $c$ and $n$) and judged that it refutes the question through the elementary bridge above. Not reviewed: no outside reviewer or independent acceptance of this route is recorded; the site's commentary credits Kahane and does not mention the release (the proof-claims tab was empty on 2026-10-07). Not refereed: the manuscripts are unrefereed release preprints with no arXiv version, whose author line names OpenAI; the release's README says that its manuscripts and proof artifacts were produced by an internal OpenAI model and that the collection includes results at different stages of verification. This page describes the pinned revision of the release only.