Erdős Problem #119
SOLVED LEANdatabase updated 2026-08-23
Resolved in some way other than a straight proof or disproof — usual for open-ended questions, or for multi-part problems whose parts went different ways. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Let \(z_i\) be an infinite sequence of complex numbers such that \(|z_i| = 1\) for all \(i \geq 1\). For \(n \geq 1\) let \(p_n(z) = \prod_{i \leq n} (z - z_i)\).
Let \(M_n = \max_{|z| = 1} |p_n(z)|\).
Is it true that \(\limsup M_n = \infty\)? This is Problem 4.1 in [Ha74] where it is attributed to Erdős. The weaker conjecture that \(\limsup M_n=\infty\) was proved by Wagner [Wa80], who show that there is some \(c>0\) with \(M_n>(\log n)^c\) infinitely often.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/119.Prize$100
Topicsanalysis, polynomials
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/119
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.