Erdős problem 1038
Among all nonconstant monic polynomials whose roots lie in , determine .
Sources
FormalConjectures/ErdosProblems/
1038.lean
Retained formal statement
What is the infimum of |{x ∈ ℝ : |f x| < 1}| over all nonconstant monic polynomials f such that all of its roots are real and contained in [-1,1]?
∀ (n : ℕ), sorry = ⨅ f, MeasureTheory.volume {x | |Polynomial.eval x ↑f| < 1}OpenStatement only, no proof