Skip to content

Erdős problem 974

Let z1,,znCz_1,\ldots,z_n\in \mathbb{C} be a sequence such that z1=1z_1=1. Suppose that the sequence of sk=1inziks_k=\sum_{1\leq i\leq n}z_i^k contains infinitely many (n1)(n-1)-tuples of consecutive values of sks_k which are all 00. Then (essentially) zj=e(j/n),z_j=e(j/n), where e(x)=e2πixe(x)=e^{2\pi ix}.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/974.lean

Formal Conjectures

FormalConjectures/ErdosProblems/974.leanErdos974.erdos_9742 linesExact file
∀ {n : ℕ} [inst : NeZero n] (z : Fin n → ℂ),  z 0 = 1 → {k | ∀ j < n - 1, ∑ i, z i ^ (k + j) = 0}.InfiniteErdos974.IsTuranConfiguration z
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:974
  • PLBY Lean proofsErdosProblems.Erdos974

Reported activity

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

Continue

Search problems.science

Find a Problem, Result, source, or page