Erdős Problem #525
PROVEDdatabase updated 2025-08-31
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The degree-`n` polynomial \(f(z)=\sum_{j\leq n}\epsilon_j z^j\) with coefficients `ε : Fin (n + 1) → ℤˣ`, i.e. \(\epsilon_j\in\{-1,1\}\), evaluated at `z`.
The degree-`n` polynomials with \(\pm 1\) coefficients such that \(|f(z)|\geq 1\) for all \(|z|=1\).
\(m(f)=\min_{|z|=1}|f(z)|\).
Is it true that all except at most \(o(2^n)\) many degree \(n\) polynomials with \(\pm 1\)-valued coefficients \(f(z)\) have \(\lvert f(z)\rvert <1\) for some \(\lvert z\rvert=1\)? The answer is yes: Littlewood [Li66] conjectured the stronger \(m(f)=o(1)\) almost surely, which was proved by Kashin [Ka87].
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 4 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/525.Prizenone
Topicsanalysis, probability, polynomials
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/525
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.