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}.

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

974.lean

Retained formal statement1 of 2

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}.

A conjecture of Turán.

This is true (in the stronger form with only two such tuples) - in fact if nn is odd then the ziz_i must be exactly the nnth roots of unity, and if nn is even they must be the vertices of two regular (n/2)(n/2)-gons with the same circumscribed circle centred at the origin. This was first proved by Tijdeman [Ti66]. An independent proof of this was given in the comments section by Hu, Tang, and Zhang.

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.

Search problems.science

Find a Problem, Result, source, or page