Erdős Problem #974
PROVED LEANdatabase updated 2026-04-27
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The configuration described by Tijdeman: if `n` is odd then the `z i` are exactly the `n`th roots of unity, and if `n` is even then they are the vertices of two regular `(n / 2)`-gons with the same circumscribed circle centred at the origin, that is, the `(n / 2)`th roots of `1` together with the `(n / 2)`th roots of some other point `c` on the unit circle.
Let \(z_1,\ldots,z_n\in \mathbb{C}\) be a sequence such that \(z_1=1\). Suppose that the sequence of \[s_k=\sum_{1\leq i\leq n}z_i^k\] contains infinitely many \((n-1)\)-tuples of consecutive values of \(s_k\) which are all \(0\). Then (essentially) \[z_j=e(j/n),\] where \(e(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 \(n\) is odd then the \(z_i\) must be exactly the \(n\)th roots of unity, and if \(n\) is even they must be the vertices of two regular \((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.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/974.Prizenone
Topicsanalysis
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/974
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.