erdős #228
Does there exist, for all large , a polynomial of degree , with coefficients , such thatfor all , with the implied constants independent of and ?
Worked, still open.
analysis · solved · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsformal
AMS 5 12 41 · solved (literature)
theorem erdos_228 :
answer(True) ↔ ∃ (c₁ : ℝ) (c₂ : ℝ), ∀ᶠ n : ℕ in Filter.atTop,
∃ p : Polynomial ℂ, p.degree = n ∧
(∀ i ≤ n, p.coeff i = 1 ∨ p.coeff i = -1) ∧
∀ z : ℂ, ‖z‖ = 1 →
( √n < c₁ * ‖p.eval z‖ ∧ ‖p.eval z‖ < c₂ * √n )formal-conjectures/228.lean ↗status
solved