Erdős Problem #1043
DISPROVED LEANdatabase updated 2025-12-28
The statement as posed is false. 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).
The set \(\{ z \in \mathbb{C} : \lvert f(z)\rvert\leq 1\}\)
**Erdős Problem 1043**: Let \(f\in \mathbb{C}[x]\) be a monic polynomial. Must there exist a straight line \(\ell\) such that the projection of \[\{ z: \lvert f(z)\rvert\leq 1\}\] onto \(\ell\) has measure at most \(2\)? Pommerenke [Po61] proved that the answer is no. The projection onto the line \(\ell = \mathbb{R} u\) is measured with the Lebesgue measure of that line, so `volume` of the projected set is its length. This was formalized in Lean by Alexeev using Aristotle.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/1043.Prizenone
Topicsanalysis
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/1043
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.