Erdős Problem 519

Theorem 519 · Erdős

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.

Formal statement · Lean 4.lean

theorem erdos_519 : answer(True) ↔
    ∃ c : ℝ, 0 < c ∧
      ∀ (n : ℕ) (hn : 0 < n) (z : Fin n → ℂ),
        z ⟨0, hn⟩ = 1 →
          ∃ k : Fin n, c < ‖powerSum z (k.val + 1)‖ := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗