Skip to content

Erdős problem 1044

Let f(z)=i=1n(zzi)C[x]f(z)=\prod_{i=1}^n(z-z_i)\in\mathbb{C}[x] where zi1\lvert z_i\rvert\leq 1 for all ii. If Λ(f)\Lambda(f) is the maximum of the lengths of the boundaries of the connected components of {z:f(z)<1} \{ z: \lvert f(z)\rvert<1\} then determine the infimum of Λ(f)\Lambda(f).

Sources

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1044.lean

Retained formal statement4 of 4

This has been resolved by Tang, who proved that the infimum of Λ(f)\Lambda(f) over all such ff is 22.

FormalConjectures/ErdosProblems/1044.leanErdos1044.erdos_1044.variants.infimum_eq_two1 lineExact file
IsGLB {L | ∃ f, Erdos1044.IsAdmissible fErdos1044.maxBoundaryLength f = L} 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.

Search problems.science

Find a Problem, Result, source, or page