Skip to content

Erdős problem 519

Let z1,…,zn∈Cz_1,\ldots,z_n\in \mathbb{C} with z1=1z_1=1. Must there exist an absolute constant c>0c>0 such that max⁡1≤k≤n∣∑izik∣>c? \max_{1\leq k\leq n}\left\lvert \sum_{i}z_i^k\right\rvert>c?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/519.lean

Formal Conjectures

FormalConjectures/ErdosProblems/519.leanErdos519.erdos_5191 lineExact file
True ↔ ∃ 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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:519
  • PLBY Lean proofsErdosProblems.Erdos519

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page