Erdős problem 990
Let be a polynomial. Is it true that, if has roots with corresponding arguments , then for all intervals where is the number of non-zero coefficients of and
Sources
FormalConjectures/ErdosProblems/
990.lean
Retained formal statement
An internal OpenAI model (see [APSSV26b]) has disproved the conjecture, constructing, for every , a polynomial with non-zero coefficients such that and with a positive real zero of multiplicity .
∀ (n : ℕ), 1 ≤ n → ∃ f, f.coeff 0 ≠ 0 ∧ f.support.card = n ∧ Erdos990.M f < 3 ∧ ∃ x, 0 < x ∧ Polynomial.rootMultiplicity (↑x) f = n - 1SolvedStatement only, no proof