Prove LittlewoodFiniteFlatness (openai/math family 076: Ultraflat real Littlewood polynomials) in Lean 4…
Prove LittlewoodFiniteFlatness (openai/math family 076: Ultraflat real Littlewood polynomials) in Lean 4…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 076 of the release, Ultraflat real Littlewood polynomials (Real and complex analysis)…
The task
Context: this statement belongs to family 076 of the release, *Ultraflat real Littlewood polynomials* (Real and complex analysis). The family as a whole: 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…
Part of raising-heart/openai-math.