Real ultraflat Littlewood polynomials and unbounded binary merit factors
OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Constructs polynomials with N consecutive coefficients in \(\{-1,1\}\) whose modulus is \((1+o(1))\sqrt N\) uniformly on the entire unit circle, for every sufficiently large integer length N. Thus real Littlewood polynomials are ultraflat, including at the real endpoints. Their binary merit factors tend to infinity, disproving Turyn’s bounded-merit-factor conjecture. (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
The independent assessments find that the Lean statements express only part of the result described above, or a narrower statement.Read the assessments
Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.
The other possible matches are Theorem 1.1 in Nearly minimal maxima and positive minima of Littlewood polynomials () and Theorem 1 in Ultraflat real Littlewood polynomials ().
For Littlewood polynomials with real coefficients,
\lim_{N\to\infty}m_N=1.
Equivalently, for every \eta>0 there is N_0 such that for every integer N\ge N_0 there are signs \varepsilon_0,\ldots,\varepsilon_{N-1} with
\max_{|z|=1}\left|\sum_{k=0}^{N-1}\varepsilon_kz^k\right|
\le(1+\eta)\sqrt N.
Reported proof verification
Two Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
For every \(\varepsilon\in(0,1)\) and every sufficiently large integer N, there is a polynomial of length N with coefficients in \(\{-1,1\}\) whose modulus lies between \((1-\varepsilon)\sqrt N\) and \((1+\varepsilon)\sqrt N\) everywhere on the unit circle. Thus real Littlewood polynomials can be ultraflat through every sufficiently large integer length. The signs may be chosen separately at each length.
For every η > 0 and every sufficiently large integer N, there is a polynomial with N consecutive coefficients in \(\{-1,1\}\) whose modulus lies between \(\sqrt N/16\) and \((1+\eta)\sqrt N\) everywhere on the unit circle.
We prove that the minimum possible maximum modulus on the unit circle of a polynomial with N consecutive real coefficients in \(\{-1,1\}\) is \((1+o(1))\sqrt N\), as N tends to infinity through all integers. This disproves the real-sign analogue of Erdős’s fixed relative-gap conjecture. As a consequence, the largest binary merit factor at length N tends to infinity through all integer lengths, disproving Turyn’s conjecture.
Two Lean statements in this family
Choose one to see it beside the paper theorem it is paired with.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
AsymptoticallyMinimalLittlewood.lean, the release lists it as a main result.
defMainStatement : Prop := ∀ η : ℝ, 0 < η → ∃ N₀ : ℕ, 1 ≤ N₀ ∧ ∀ N : ℕ, N₀ ≤ N → ∃ ε : Fin N → ℝ, IsRealSigning ε ∧ ∀ z : ℂ, ‖z‖ = 1 → ‖littlewoodValue ε z‖ ≤ (1 + η) * Real.sqrt N⋮theoremmain : MainStatement := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.
LittlewoodFiniteFlatness.lean, the release lists it as a supporting statement.
defMainStatement : Prop := ∃ ε : (N : ℕ) → Fin N → ℝ, (∀ N : ℕ, IsRealSigning (ε N)) ∧ ∀ p : ℝ, 0 < p → Filter.Tendsto (fun N : ℕ => ∫ t : UnitAddCircle, Real.rpow |‖littlewoodValue (ε N) (fourier (1 : ℤ) t)‖ / Real.sqrt (N : ℝ) - 1| p ∂AddCircle.haarAddCircle) Filter.atTop (𝓝 (0 : ℝ))⋮theoremmain : MainStatement := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.
Other mathematical statements in OpenAI’s Lean library
Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.
Independent comparisons and proof-verification reports
Does the Lean express the advertised result?
Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express a weaker statement than the advertised result (their term: “weaker-statement”).
Their note:Only max-modulus <= (1+eta)sqrt(N) and L^p (finite p) flatness are stated; uniform ultraflatness (two-sided, sup norm), merit factor -> infinity and the disproof of Turyn’s conjecture are not. Two of the three index papers (Oct 5) are not linked in docs.
“weaker-statement”, in their words: The challenge statements do not imply the headline claim: they state a nontrivially weaker statement.
Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — UNLINKED”).
The gap they name:The lower half of ultraflatness — min over |z| = 1 of |P_N(z)| ≥ (1−ε)√N for every large N, including z = ±1 — is not stated; the Lean gives the upper bound and finite-p L^p flatness only. The merit-factor clause is implied, not stated.
“NARROWER — UNLINKED”, in their words: The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.
Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
The formalization gives real Littlewood polynomials of every sufficiently large length whose maximum modulus on the unit circle is at most $(1+\eta)\sqrt N$ for any fixed $\eta>0$. Thus the smallest possible maximum is asymptotically minimal through all integer lengths.
A further statement chooses one family of real sign polynomials for all lengths such that, for every fixed finite $p>0$, the $L^p$ mean of $\bigl||P_N(z)|/\sqrt N-1\bigr|$ on the unit circle tends to zero. The results are existential and do not give an effective convergence rate or a signing algorithm.
AI-drafted comparisons, with no recorded human review
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: for every η > 0 and every large length N there is a real Littlewood polynomial with maximum modulus at most (1 + η)√N on the unit circle.
Finite-exponent flatness of one all-length Littlewood familyLittlewoodFiniteFlatness
Unreviewed AI draft: states a consequence of a paper’s theorem. States the paper’s finite-exponent flatness corollary (Section 7): one sign family of every length with ||P_N|/√N − 1| tending to 0 in every L^p, p < ∞. The two-sided ultraflat bound of the family’s later paper is not part of the statement.
Who ran the proof-verification program?
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
What these papers cite in the release, and what cites them
These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
Papers elsewhere in the release that cite this family’s papers
No paper elsewhere in the release cites this family’s papers.
Follow-up work by others
The Justin Sun Prize, The Justin Sun Prize: problem bank and award records, 11 October 2026. Source
JSP-000955 lists the release’s claim as Solved with independent mathematical review pending; Lean proof column: reported complete, independent verification pending.
anxkhn, Series of 15 issues and 15 draft PRs adding release results to Formal Conjectures (issues 6972 to 6997, PRs 6977 to 7002), 8 October 2026. Source
Proposes adding the release’s asymptotically minimal maxima of real Littlewood polynomials to Formal Conjectures (issue 6986, PR 6991).
References outside the release
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Explain a result, compare statements or propose a correction
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a counterexample and rates its significance, if it holds up, as “Career-defining publication”. The page says that nothing on it is verified.
VibeMathed, VibeMathed: math problems solved with AI, 11 October 2026. Source
Contested: conflicts with preprints by el Abdalaoui (arXiv:1609.03435 and two others) claiming flat Littlewood polynomials of this kind do not exist.
Moritz Firsching, anxkhn, Paul Lezeau, Formal Conjectures: mark problems solved in the OpenAI math release and link formal proofs, 11 October 2026. Source
A Formal Conjectures maintainer, after source inspection, links the Littlewood polynomial result to Erdos problem 1150, recording a length against degree difference.
tparker, Philip Weiss, Will Sawin, Nik Weaver, Pace Nielsen, mathworker21, Joshua P. Swanson, Timothy Chow, Daniel Soltesz, MathOverflow: how many of the released results went against the conventional wisdom?, 9 October 2026. Source
An answerer says many people expected that no ultraflat Littlewood polynomial would exist.
Thomas Bloom, Erdős problems in the OpenAI proofs, 8 October 2026. Source
Bloom lists Erdős 1150 (ultraflat Littlewood polynomials), names Balister, Bollobás, Morris, Sahasrabudhe and Tiba, and notes it relies on two other PDFs of the release.
Questions awaiting review
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Read the Lean statement against the paper
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
Identify the theorem the catalogue describes
Family 076The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means.Open the form
Compare the proposed paper and Lean matches
Family 076Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing.Open the form
Why this passage is shown
Theorem 1.1
In Nearly minimal maxima and positive minima of Littlewood polynomials, 5 October 2026
How it was found
Its words were compared with the words of OpenAI’s catalogue description.
Words they share
integer, real
Review
Atlas records no review confirming that this is the theorem OpenAI’s description refers to.
The challenge statements do not imply the headline claim: they state a nontrivially weaker statement.
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.
The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners…
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator with Lean’s kernel: accepted (the check took 172 s; peak memory 6.4 GiB).
Date
10 October 2026
Version
at the release’s recorded version
Their method
Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator with Lean’s kernel: accepted (the check took 395 s; peak memory 6.4 GiB).
Date
10 October 2026
Version
at the release’s recorded version
Their method
Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
Finite-exponent flatness of one all-length Littlewood family
Role
the release lists it as a supporting statement
Paired with
Theorem 1.1 (candidate pairing)
Who ran the proof-verification program
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.