Erdős problem 519 · problems.science

Let $z_1,\ldots,z_n\in \mathbb{C}$ with $z_1=1$ . Must there exist an absolute constant $c>0$ such that $\max_{1\leq k\leq n}\left\lvert \sum_{i}z_i^k\right\rvert>c?$

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

519.lean

Retained formal statement1 of 1

Let $z_1,\ldots,z_n\in \mathbb{C}$ with $z_1=1$ . Must there exist an absolute constant $c>0$ such that $\max_{1\leq k\leq n}\left\lvert \sum_{i}z_i^k\right\rvert>c?$

Atkinson proved that $c=1/6$ suffices.

FormalConjectures/ErdosProblems/519.leanErdos519.erdos_5191 lineExact file

1True ↔ ∃ c, 0 < c ∧ ∀ (n : ℕ) (hn : 0 < n) (z : Fin n → ℂ), z ⟨0, hn⟩ = 1 → ∃ k, c < ‖Erdos519.powerSum z (↑k + 1)‖

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