we-solve (beta)

Math-2500-A1 · revision r1 · on Math-2500

OpenAI claim summary for Math-2500

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status at unsolvedmath.com: partially solved. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

For $N=n+1$ coefficients, the ultraflat claim gives $|P_N|/\sqrt N\to1$ uniformly on the circle along suitable real-sign polynomials. Their normalized Mahler measure tends to one. Jensen and the exact $L^2$ norm bound it by one for every sign polynomial, so the claimed extremal limit superior with the catalogue normalization $\sqrt n$ is $b_m=1$.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Maximum Normalized Mahler Measure of Littlewood Polynomials
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Mathematical claim 1.
  5. Mathematical claim 2.
  6. Mathematical claim 3.
  7. Outline of the argument
  8. Formal verification
  9. Status caveat
  10. Sources

Maximum Normalized Mahler Measure of Littlewood Polynomials

OpenAI's claim

Nearly optimal Littlewood maxima: The optimal supremum norm of a real sign polynomial of length $N$ is claimed to approach $\sqrt N$ relatively, with $N$ running through every integer; the resulting binary sequences have merit factors tending to infinity.

Littlewood polynomials with a lower margin: The paper claims sign polynomials at every sufficiently large length with maximum at most $(1+\eta)\sqrt N$ and minimum at least $\sqrt N/16$, for any fixed positive $\eta$; both inequalities concern the same polynomial.

Uniformly flat real sign polynomials: OpenAI claims that real sign polynomials can have normalized modulus uniformly as close to one as desired once the integer length is large enough; choices at different lengths are independent of one another.

Mathematical statement of the claimed result

Mathematical claim 1.
For each $\eta>0$, all sufficiently large integers $N$ admit signs $\epsilon_k\in\{-1,1\}$ such that the real Littlewood polynomial $P_N(z)=\sum_{k=0}^{N-1}\epsilon_kz^k$ obeys \[\max_{|z|=1}|P_N(z)|\le(1+\eta)\sqrt N.\] Thus the minimum possible normalized maximum $m_N=\min_{\epsilon_k=\pm1}\max_{|z|=1}|P_N(z)|/\sqrt N$ tends to $1$. This result gives an upper maximum, without a pointwise lower bound.
Mathematical claim 2.
Given $\eta>0$, there is $N_0(\eta)$ such that for every integer $N\ge N_0(\eta)$ one can choose real signs $\epsilon_0,\ldots,\epsilon_{N-1}$ with \[\frac{\sqrt N}{16}\le\left|\sum_{k=0}^{N-1}\epsilon_kz^k\right|\le(1+\eta)\sqrt N\quad(|z|=1).\] The same polynomial has both bounds uniformly on the circle; the lower constant is $1/16$.
Mathematical claim 3.
For every $0<\epsilon<1$, all sufficiently large integers $N$ admit signs $a_k\in\{-1,1\}$ such that \[(1-\epsilon)\sqrt N\le\left|\sum_{k=0}^{N-1}a_kz^k\right|\le(1+\epsilon)\sqrt N\quad\text{for all }|z|=1.\] The quantifier covers every sufficiently large length, and both inequalities refer to one polynomial.

Outline of the argument

Nearly optimal Littlewood maxima: The construction starts with bounded real coefficients obtained by sampling quadratic-phase waves on an auxiliary torus. Interval packing separates the relevant frequency ranges and keeps almost all of the mean-square mass. A discrepancy rounding step changes the coefficients to signs while keeping the circle supremum error small compared with $\sqrt N$; Parseval’s identity then supplies the lower comparison.

Littlewood polynomials with a lower margin: The relaxed-coefficient construction for small maxima is augmented on arcs where its leading amplitude is too small. Carefully matched quadratic phases create a positive lower margin without introducing excessive Fourier coefficients outside the permitted degree range. A rounding estimate expressed in terms of the remaining coefficient defect preserves the margin while turning the coefficients into signs.

Uniformly flat real sign polynomials: A continuous circle function is built with nearly constant modulus, real coefficients of nearly sign size in the retained frequency range, and a small Fourier tail. Auxiliary-torus waves and phase corrections coordinate the upper and lower modulus bounds. Parseval controls the aggregate coefficient defect, allowing discrepancy rounding to preserve uniform flatness.

Formal verification

Family 076 describes Lean coverage for near-minimal upper maxima and convergence of finite-exponent modulus means; the later uniform lower-envelope conclusions are separate.

Nearly optimal Littlewood maxima: The manuscript links AsymptoticallyMinimalLittlewood.lean (declaration OAI.AsymptoticallyMinimalLittlewood.main), LittlewoodFiniteFlatness.lean.

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

Littlewood polynomials with a lower margin: No manuscript-specific Comparator is listed in the pinned inventory.

The documented selection does not cover the entire manuscript assertion relevant here.

Uniformly flat real sign polynomials: No manuscript-specific Comparator is listed in the pinned inventory.

The documented selection does not cover the entire manuscript assertion relevant here.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources