OAI.AsymptoticallyMinimalLittlewood.main

Open

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that for every real number η > 0 there exists an integer N₀ ≥ 1 such that, for every integer N ≥ N₀, one can choose real coefficients ε₀, …, ε_{N−1}, each equal to either −1 or 1, so that the Littlewood polynomial P(z) = ∑_{k=0}^{N−1} εₖzᵏ satisfies |P(z)| ≤ (1 + η)√N for every complex number z on the unit circle. The choice of coefficients may depend on N and η, but the bound holds uniformly over all |z| = 1.

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/AsymptoticallyMinimalLittlewood.lean; bytes 536..578
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_AsymptoticallyMinimalLittlewood

namespace OAI

namespace AsymptoticallyMinimalLittlewood

Formal statement

theorem main : MainStatement := by
  sorry

end AsymptoticallyMinimalLittlewood
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/AsymptoticallyMinimalLittlewood.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by marwahaha · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph