Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


R. Tijdeman, On a conjecture of Turán and Erdös, Indag. Math. (Proceedings) 69 (1966), 374-383, proves Turán's conjecture in the stronger form Erdős suggested. Let z1,…,zn∈Cz_1,\ldots,z_n\in\mathbb C be pairwise distinct with z1=1z_1=1, let sk=∑i≤nziks_k=\sum_{i\le n}z_i^k, and suppose that two distinct runs of n−1n-1 consecutive indices kk have sk=0s_k=0. Then, when nn is odd, the ziz_i are exactly the nnth roots of unity, and, when nn is even, they are vertices of two regular (n/2)(n/2)-gons inscribed in one circle centered at the origin. (The site's thread records that Tijdeman assumes the ziz_i pairwise distinct. A single run of n−1n-1 vanishing power sums already forces the ziz_i to be pairwise distinct and nonzero by a Vandermonde argument, the first step of Proposition 1 of Hu, Tang and Zhang in the thread, so the classification holds as the problem states it, without that hypothesis; both Lean files prove this step.) This is the meaning the site gives the word "essentially" in the problem's conclusion: taken literally, zj=e(j/n)z_j=e(j/n) fails for even nn, since z1=1z_1=1, z2=iz_2=i gives sk=1+iks_k=1+i^k, which vanishes for every k≡2(mod4)k\equiv 2\pmod 4. The classification is stated here as the site and its thread give it; the paper's bibliographic record gives only the year, which the page's nominal date reflects.

Reviewed. The site's curator, Thomas Bloom, marks Problem 974 proved and credits Tijdeman's paper in the site's commentary (last edited 1 October 2025). Replying in the site's thread on 20 September 2025 to the example z1=1z_1=1, z2=iz_2=i for n=2n=2, Bloom wrote that it "is not a counterexample though", given how vaguely the problem is described.

Refereed. Indagationes Mathematicae (Proceedings) 69 (1966), 374-383, the journal publication the site's reference [Ti66] names.

Later proofs and formalizations. An independent proof was posted in the site's thread in September 2025 by Hu, Tang and Zhang, in comments and in a repository (https://github.com/taohu-hub/ErdosProblem-974) whose manuscript treats the odd case, before the thread identified Tijdeman's paper; the site credits Tijdeman, so that later proof of the same result is disclosed here and has no page of its own. A Lean 4 proof that starts from that Proposition 1 and follows Tijdeman thereafter was posted on 27 April 2026 by Jeremy Tan Jie Rui (GitHub login Parcly-Taxel) as a gist, and Boris Alexeev's lean-proofs repository re-hosts it with a header naming Tijdeman and Tang as informal authors and Aristotle and Tan as formal authors. The corpus has built neither file, so the claim lists no formalized evidence.