Erdős problem 1038
Among all nonconstant monic polynomials whose roots lie in , determine .
Sources
FormalConjectures/ErdosProblems/
1038.lean
Retained formal statement
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] is < 1.835.
∀ (n : ℕ), ⨅ f, MeasureTheory.volume {x | |Polynomial.eval x ↑f| < 1} < 1.835SolvedStatement only, no proof