Erdős problem 509
Let be a monic non-constant polynomial. Can the set be covered by a set of closed discs the sum of whose radii is ?
Sources
FormalConjectures/ErdosProblems/
509.lean
Retained formal statement
Let be a monic non-constant polynomial. Can the set be covered by a set of closed discs the sum of whose radii is ?
True ↔ ∀ (f : Polynomial ℂ), f.Monic → f.natDegree ≠ 0 → ∃ ι, Nonempty (Erdos509.BoundedDiscCover {z | ‖Polynomial.eval z f‖ ≤ 1} 2 ι)OpenStatement only, no proof