Erdős problem 1043 · problems.science

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$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1043.lean

Retained formal statement1 of 2

Pommerenke [Po61] proved that the answer is no.

This was formalized in Lean by Alexeev using Aristotle.

FormalConjectures/ErdosProblems/1043.leanErdos1043.erdos_10434 linesExact file

1False ↔2  ∀ (f : Polynomial ℂ),3    f.Monic →4      f.degree ≥ 1 → ∃ u, ‖u‖ = 1 ∧ MeasureTheory.volume (⇑(ℝ ∙ u).orthogonalProjection '' Erdos1043.levelSet f) ≤ 2

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science