#1150: OpenAI answers Erdős's ultraflat question for ±1 polynomials with NO — the Lean states the theorem that negates what was asked, our kernel replay printed the three standard axioms, and seven hostile seats read the proof and the ultraflat paper: no gap

The problem (erdosproblems.com/1150; Hayman's 1974 problem list 4.31, the 1999 Budapest "Paul's favorite problems" booklet 2.36; Erdős and Newman's question of the 1950s–70s — on the problem page a commenter cites Erdélyi for a $100 prize, which the tracker does not record). Is there a constant c > 0 such that, for all large n and every polynomial P of degree n with coefficients ±1, max_|z|=1 |P(z)| > (1 + c)√n? Parseval gives √(n+1) for free, so the question is whether the real-sign ("Littlewood") class is forced a fixed fraction above that floor. For complex coefficients of modulus one the analogous conjecture is false — Kahane's ultraflat polynomials (1980), erdosproblems.com/230 — and the ±1 case has stood since: Rudin–Shapiro gives max ≤ √(2N) at dyadic lengths, Balister, Bollobás, Morris, Sahasrabudhe and Tiba (Annals 2020) proved two-sided flatness with fixed constants at every degree n ≥ 2, and Erdélyi's August 2026 preprint (arXiv:2608.00744) proves max² ≥ N + (N−1)^1/3/38 while still treating the fixed-gap question as open. The teorth database says OPEN (last updated 23 January 2026); the page was last edited the same day.

What OpenAI's 6 October release claims, in three strengths — keep them apart. Family 076 of the release is three papers. (1) "Asymptotically minimal maxima of real Littlewood polynomials" (23 September 2026, 26 pages; sha256 3f6f94e6… in our bundle): Theorem 1.1, lim_N→∞ m_N = 1, where m_N is the least normalized maximum over all 2^N sign choices at length N — equivalently, for every η > 0 and every sufficiently large length N there are signs with max_|z|=1 |Σ ε_kz^k| ≤ (1 + η)√N. One-sided (no lower bound on |P|), every length rather than a subsequence, no rate, no algorithm. This alone implies the negation of #1150, by one elementary line: given any c > 0 take η = c/2; a length-N Littlewood polynomial has degree n = N − 1, and (1 + c/2)√(n+1) ≤ (1 + c)√n once n is large, so no c works. (2) "Nearly minimal maxima and positive minima" (5 October, 28 pages): √N/16 ≤ |P| ≤ (1 + η)√N on the whole circle. (3) "Ultraflat real Littlewood polynomials" (5 October, 16 pages): (1 − ε)√N ≤ |P| ≤ (1 + ε)√N everywhere, for every large N — the family's headline, and more than #1150 asks. Only (1) is formalized; (2) and (3) are paper-only, and nothing below about them changes the scoreboard. A corollary of (1) the paper draws in §8: the largest binary merit factor at length N tends to infinity through all lengths, which would refute Turyn's conjecture (equivalently Erdős's L⁴-norm conjecture) — a second famous question, settled negatively in passing if Theorem 1.1 holds.

The Lean, and what it says. The Comparator challenge ComparatorChallenges/AsymptoticallyMinimalLittlewood.lean states ∀ η : ℝ, 0 < η → ∃ N₀ : ℕ, 1 ≤ N₀ ∧ ∀ N : ℕ, N₀ ≤ N → ∃ ε : Fin N → ℝ, IsRealSigning ε ∧ ∀ z : ℂ, ‖z‖ = 1 → ‖littlewoodValue ε z‖ ≤ (1 + η) * Real.sqrt N, with IsRealSigning ε := ∀ k, ε k = -1 ∨ ε k = 1 and littlewoodValue ε z := ∑ k : Fin N, (ε k : ℂ) * z ^ (k : ℕ) — Theorem 1.1 in the paper's own "equivalently" form, plus a harmless 1 ≤ N₀ clause; every length, both endpoints included since ‖z‖ = 1 ranges over the whole circle. The solution module is OAI/Analysis/Littlewood/Main.lean, theorem main : MainStatement; the catalogue's permitted axioms are the three standard ones, enable_nanoda: false. A second comparator, LittlewoodFiniteFlatness.lean, formalizes the paper's Corollary 7.1 (one sign family for all lengths, L^p-flat for every finite p > 0). The two-sided papers are not formalized at all — OpenAI's own scope note (lean/docs/076.md) lists only the 23 September paper. Our source audit, 12 October: the import cone of Main is 24 modules and 9,315 lines, all under OAI/Analysis/Littlewood/ and importing nothing but Mathlib (28 modules and 9,712 lines with FiniteFlatness, which adds one OpenAI measure-theory module and two Lean-core tactic imports); a scan of the 27 Littlewood files (9,601 lines) finds zero occurrences of sorry, admit, native_decide, implemented_by, @[extern, unsafe, opaque, partial def, maxHeartbeats and no axiom declarations (the word occurs once, in a docstring); the scan's positive control (a planted sorry) fires. MainStatement, littlewoodValue and IsRealSigning in the solution's Model.lean are textually the challenge's (two docstrings differ), each defined once in the cone, and theorem main : MainStatement at Main.lean:187 can resolve to nothing else; all 27 Littlewood files are byte-identical between the pinned revision adc7f124 and the repository's current head. One structural fact our Lean seat found that the paper does not say: the formal proof follows §§2–6 step for step but replaces two of the paper's cited inputs and one of its own analytic steps — Pippenger–Spencer (Theorem 3.2, not in Mathlib) by an in-house Rödl-nibble almost-perfect matching under a stronger codegree condition the finite-field hypergraph happens to satisfy; Lovett–Meka (Lemma 6.1) by the classical entropy partial colouring; and the grid-to-circle step by a Dirichlet-kernel Cauchy–Schwarz argument instead of the maximum principle — with stationary phase built from Mathlib's Gaussian Fourier identity and Poisson summation from SchwartzMap.tsum_eq_tsum_fourier. So a kernel pass certifies Theorem 1.1 and nothing about the paper's two combinatorial citations; the statement is not vacuous (at N = 2 the best maximum is 2, so the bound fails there for η < √2 − 1, forcing N₀ > 2), signings exclude 0, and the quantifier order is η → δ → data → C → N₀ → N.

Our kernel replay — green. Theorem 1.1 is the kind of claim a kernel can settle, so we did not stop at reading. On this machine, on 12 October (09:24–09:40Z), the 28-module import cone of OAI.Analysis.Littlewood.Main and FiniteFlatness was compiled from the pinned sources (OpenAI adc7f124, Mathlib d13f23b7, Lean 4.34.1) with the toolchain's own lean, one module at a time in import order at two threads and the lowest priority, writing object files into a directory of ours — 28 of 28 built in 952 s, zero error lines in every module log — then a probe importing both modules was run under --trust=0: 'OAI.AsymptoticallyMinimalLittlewood.main' depends on axioms: [propext, Classical.choice, Quot.sound], and the same three for AsymptoticallyMinimalLittlewoodFiniteFlatness.main — the three standard axioms Mathlib uses, and nothing else: no sorryAx, no custom axiom. Three controls ran in the same session: the comparator file itself, compiled the same way with its sorry in place, reports [propext, sorryAx, Classical.choice, Quot.sound]; a bare sorry'd theorem reports [sorryAx]; and the pp.all printouts of MainStatement, littlewoodValue and IsRealSigning taken from the solution build and from the challenge build are byte-identical (STATEMENT MATCH). So the kernel accepted, on a machine OpenAI does not control, a proof of exactly the statement whose truth answers erdosproblems.com/1150 with no. This entry is CLOSED — not ours: the theorem is OpenAI's and so is the formal proof — and #1150 joins the problems closed in the literature, answer NO. One outside machine check of the same Lean with a published log exists (carlostoledo1891/cert-machine, 10 October, Lean and nanoda kernels, 8,947 jobs) and one is claimed without a log (plasma-ai/erdos, 7 October) — neither a human review, and ours is independent of both. How this run was shaped, for the record: the replay was first queued as a lake build behind our running #3 replay in the same workspace, which would have held it for an estimated five hours; it was retired without building anything and replaced by the direct compile above, which takes the exact LEAN_PATH and the single option (-DautoImplicit=false) that Lake hands its own compiler jobs and touches nothing in the shared workspace (the first direct attempt failed on Lean's root-directory rule — wrong working directory — and is in steps.tsv as such). One honest limit, the same one as on #172, #181 and #1083: in Lean 4.34 --trust=0 no longer re-checks imported modules, so what this run kernel-checked from source is the proof itself, while Mathlib's object files came from the cache; the leanchecker --fresh pass over Main's import closure, Mathlib included, started at 09:40Z on 12 October and exited 0 after 6,978 s (1 h 56 min) at 11:36Z, printing only Lake's "has local changes" warnings and no error line; the two controls for reading that silence as a pass ran on the same build (replay/leanchecker_controls.log): a module that does not exist exits 1, a real module exits 0 printing nothing. So Mathlib's cached object files are kernel-checked too, and nothing in the import closure was rejected.

The seven seats, 12 October (Opus, tool-equipped, disjoint scopes, each briefed to refute and to quote the sentence it objects to; brief and verbatim scopes in the bundle; the reports are long and every objection carries its page). reduce (§1–2, §7, Appendix A and the three contrary preprints): Theorem 1.1 = the comparator statement = a NO to #1150; every step of the §2 deduction re-derived (1 − 8δ ⇒ µ ≤ 4δN; u log(80N/u) increases up to 80N/e; limsup m_N is δ-free so δ ↓ 0 after N → ∞ is legitimate); Corollary 7.1 holds for every finite p and, correctly, not for p = ∞; neither §7 nor Appendix A is used in the proof (grep-confirmed); Appendix A's three diagnoses checked against the preprints themselves — arXiv:2504.21499's equation (27) only gives concentration near 0, which Bonami–Révész's own Definition 2, Theorem 7 and the remark after Proposition 9 show cannot contradict c_2p ≤ ½ (the same point Bloom made on the problem page); arXiv:2509.04212's Theorem 1 is false as stated (the paper's a_j = 2^j² example verified exactly for n ≤ 13) and its Corollary 3 identity is misprinted and false even when repaired; arXiv:1609.03435v2's equation (2.1) does fix both end signs, so the 4/√N repair is right. construct (§3–4): every inequality of Lemma 3.1 re-derived (ranks over F_q, p = 1/(2L), degrees and codegrees (7)–(8), the exceptional set, the collision bound, the Chebyshev–Markov deletion and the matching size); pairwise non-parallelism suffices because only sums and differences of two forms decide a collision; the ±a centres never coincide (2c ≢ 0 mod q); Alon–Yuster's Lemma 2.1 fetched from the author's PDF and the paper's Theorem 3.2 matches it (the 1989 Pippenger–Spencer original is paywalled and was not fetched; it reportedly carries an extra D ≥ D₀ hypothesis, harmless here); Lemma 4.2's error constant is explicit, π‖ξ²ĝ‖₁/(T|β|), checked numerically; Proposition 4.1's |F| ≤ 1, ‖F‖₂ ≥ 1 − 3δ and |F̂(a)|²/|λ_a| ≤ K_δ² re-checked; the choice order δ → d → S → γ → b → τ → g → B → F, A, v → L_i → q → H, θ_h → cutoffs → N is acyclic and nothing in §3–4 depends on N. sample (§5): Lemma 5.1 line by line (Poisson step, integer shifts, both integrations by parts, the stationary point), uniform in the angle (b ∈ J) because Lemma 4.2's error does not depend on u, the block centres being fixed data, finitely many; at most one stationary contribution per angle because a nonzero term forces a strict inequality, the packed intervals are pairwise disjoint, and each is shorter than one; all three mean-square cases re-derived, and (1 − δ)(1 − 3δ)² ≥ 1 − 7δ; a vector for every N ≥ 1 with no rounding of N/H; a toy run of the full §5 construction converges to the predicted maximum and matches the predicted mean square, and both negative controls fire (overlapping intervals add the peaks; κ = 0 with β ∈ ℤ doubles the mean square). round (§6, §8): Lemma 6.1 matches Lovett–Meka's Theorem 4 in arXiv:1203.5747v2 (the version cited: same thresholds — the sum is exactly u/16 — row-norm scaling, half the coordinates fixed, existence by continuity; C₀ ≈ 33.9 absolute); the dyadic rounding's sign reversal keeps µ non-increasing and the step errors sum to C₀/(√2 − 1)·√(µ log(80N/µ)); µ = 0, tiny µ and N = 1 all work; §8's merit-factor normalization equals Downarowicz–Lacroix's 1/(2M_A), Corollary 8.1 follows for every length, brute force over all words with N ≤ 12 agrees, and Corollary 8.2 is the forward direction of their Theorem 2 with "simple spectrum" meaning the same thing in both papers. lean: the findings in the Lean paragraph above, plus a vacuity sweep (none) and the formal Proposition 2.1 being stronger than the printed one (the bound K_δ + C/N at every N ≥ 1). ultra (the 16-page two-sided paper, not needed for #1150): every step of its §2–6 re-derived from the rendered PDF; the lower bound is uniform across the gaps by construction (|B_N| = m_j ≥ 1 on every gap, the gaps cost only on the Fourier side, and matching the phase derivatives is what makes the exterior tail O(1/N)); the two lemmas inherited from the 28-page paper are quoted faithfully and applied within their hypotheses; numeric toy checks agree and their negative controls fail as they should. world (citations, numerics, the world): all 23 bibliography entries exist and every arXiv version cited is the current one; brute-force m_N for 2 ≤ N ≤ 20 (1.146 to 1.433, rigorous up to float rounding) matches Odlyzko's exhaustive Figure 1 where they overlap (N = 11 to 20, to plot resolution); Erdélyi's Theorem 2.1 is transcribed exactly and holds with slack; Appendix A's three computations are right; Jedwab–Katz–Schmidt's 6.342061… recomputes. Verdict: seven of seven HOLDS AS READ IN SCOPE; no FATAL, no GAP, no constant cycle; twenty-six exposition notes. The ones worth repeating: "[12, Problem 22]" on p. 2 attaches Erdős's 1957 list to the wrong clause — Problem 22 there is the complex-unimodular question (erdosproblems.com/230), as the problem page's commenter suspected; the real-sign sources are Hayman–Lingham 4.13/4.31, quoted correctly (and the ultraflat paper's "[8, Problem 26]" is right — Problem 26 is the two-sided ±1 question); the overview's "o(√N)" rounding loss is a small multiple of √N for fixed δ, o(√N) only as δ ↓ 0; the symbols β, L, J and µ are each overloaded; and one scholarly omission — the paper never cites Odlyzko's 2018 exhaustive search (n ≤ 52, skew-symmetric to 104), whose stated conclusion was "the computations reported here suggest that M ≈ 1.27 … these conjectures imply that ultraflat polynomials in U_n do not exist". Theorem 1.1 says M = 1: the observed plateau at 1.27–1.33 for n ≤ 100 is pre-asymptotic, and the numerics pointed the other way. (Separately, Figure 16 of Georgiev–Gómez-Serrano–Tao–Wagner plots small-degree values below the exhaustive minimum — ≈ 1.10 at degree 11 against a true 1.2808 — consistent with a mesh-evaluation defect in that paper, not in this one.) What this is not: a human expert's reading; the seats' skim lists are the edge of it — and here, unlike #3, the kernel-checked object is the statement #1150 turns on, so the reading is the second instrument, not the only one.

Our own reads. §2 (the reduction: Proposition 2.1 with K_δ = √((1+δ)³/(1−δ)) and the energy bound 1 − 7δ; Lemma 2.2 with the explicit √(µ log(80N/µ)) error, µ the defect mass ½Σ(1 − |X_k|); the deduction of Theorem 1.1 — 1 − |x| ≤ 1 − x² gives µ ≤ 4δN, the limit in N is taken with δ fixed and only then δ ↓ 0, and the lower bound m_N ≥ 1 is Parseval); §6.2 (the dyadic rounding — reversing all the signs of a partial colouring at once keeps the defect mass non-increasing, which is the whole trick, and the passage from a 20N-point grid to the circle is a Cauchy estimate with constant πe/20 < 1); and §7, Corollary 7.1 (∫f⁴ ≤ ‖f‖_∞²∫f² and Parseval give ∫(f² − 1)² → 0; |u − 1|⁴ ≤ |u² − 1|² for u ≥ 0 closes it for p ≤ 4, the eventual uniform bound for p > 4). These are the elementary ends of the paper and they are correct as written; the construction in §§3–5 and the discrepancy input in §6.1 are what the seats read.

The world, 12 October. The teorth database still says OPEN (statement formalized; last updated 23 January 2026 — we refreshed it today). erdosproblems.com/1150 carries five comments and no proof claim: in February 2026 a reader surfaced el Abdalaoui's preprint arXiv:2504.21499 claiming the affirmative — no ultraflat Littlewood polynomials — and Bloom replied that it has "multiple serious issues … the final step of the proof on page 9 does not contradict Lemma 5, since the latter is just about the existence of one function with concentration, rather than proving concentration for all functions", with Tao adding that its claims are "unconfirmed until the preprint is published (or … a Lean formalization)"; el Abdalaoui answered on 16 August 2026 defending the constant's definition. OpenAI's Appendix A names the same quantifier defect, in the same place, and two more in the later arXiv:2509.04212. Nobody on the page has mentioned the OpenAI release; it is among the 25 problems in Bloom's 8 October blog post, listed as a claim under his explicit non-endorsement (he summarizes the one-sided bound and links the 16-page PDF); Gil Kalai's 7 October round-up lists the ultraflat claim under his blanket caveat. Formal Conjectures has already moved: PR #6898, merged 11 October (the same PR that marked erdos_3 solved on source inspection), changed erdos_1150 to answer(False) and linked Main.lean#L187; its statement is the predicate it has carried since February 2026, and nobody has formalized the one-line bridge from OpenAI's comparator to it (our Lean seat sketches it: length N ⇒ degree N − 1 exactly, since no coefficient is 0). openai/math has Issues disabled; its only pull request says the Lean builds were not run. Our world seat, searching separately, found no human expert verification or refutation of family 076 anywhere it looked (Tao's blog and Mathstodon since 3 September, Erdélyi, el Abdalaoui, Balister, Sahasrabudhe, Jedwab, Katz, Schmidt, arXiv, Hacker News, Wikipedia — whose "Littlewood polynomial" page, edited 12 October, still says the ±1 problem "remains open in the peer-reviewed literature"): three reactions only — Bloom's post ("not … any kind of endorsement"), Kalai's announcement, and a MathOverflow answer of 9 October by mathworker21, "I, and I think many others, thought there would be no ultraflat Littlewood polynomial." No 076 file has been revised or withdrawn since the pin; el Abdalaoui's three preprints and Erdélyi's are un-revised.

Labels. Theorem 1.1, and with it the answer NO to Erdős #1150: (d) computer-assisted — a kernel-checked proof exists, written by the claimant, source-audited here, and our own replay printed the same three standard axioms on a statement matched to the challenge; the one-line bridge from "length N, (1 + η)√N" to the problem page's "degree n, (1 + c)√n" is (a) elementary and is written out above. The paper as written: (c) plausible/unverified by a human — five tool-equipped machine seats with disjoint scopes read its mathematics, each briefed to refute, and found no gap (two more read the ultraflat paper and the citations and numerics); and the kernel-checked proof follows the paper while substituting its own combinatorial inputs for two of the paper's citations, so the citations as such (Pippenger–Spencer via Alon–Yuster; Lovett–Meka) rest on the seats' source checks, which passed. The two-sided ultraflat theorem (1 ± ε)√N: (c) — paper-only, one seat on its chain, no kernel. The √N/16 lower bound of the 28-page paper: not refereed — only the two lemmas the 16-page paper inherits from it were read, as inputs. The merit-factor corollary that refutes Turyn's conjecture: (b) rigorous modulo Theorem 1.1 — an elementary deduction, read by the round seat. Scoreboard: #1150 → CLOSED, answer NO, not ours (OpenAI's theorem, OpenAI's formal proof, replayed here). The teorth database still says OPEN; Formal Conjectures already says answer(False); neither cites a replay, and this page does.