---

Claim. The answer to Problem 519 is yes, with $c=1/6$. F. V. Atkinson, On sums of powers of complex numbers, Acta Math. Acad. Sci. Hungar. 12 (1961), no. 1--2, 185--188, doi:10.1007/BF02066680, digested on its library card, proves (equation (3)) that for complex numbers $z_1,\ldots,z_n$ with $1=z_1\ge\lvert z_2\rvert\ge\cdots\ge\lvert z_n\rvert$, the paper's condition (1),

$$\max_{1\le k\le n}\Bigl\lvert\sum_{m=1}^n z_m^k\Bigr\rvert>\frac16,$$

with no claim that $1/6$ is best possible. The hypothesis is the site's normalization $z_1=1$ together with maximum modulus one; the site's hypothesis alone is equivalent, since a tuple with $z_1=1$ can be divided by a member of maximum modulus, which does not increase any power sum, and the quotient, whose member of maximum modulus is $1$, can be relabeled so that it comes first (the reduction recorded on the Biró 1994 card). Turán had proved a bound of order $1/n$, and the question asks whether a bound independent of $n$ exists; Atkinson's theorem is the first such bound. The proof writes the exponential of the power sum generating series as a product plus a tail of higher powers, reads the tail's coefficients as Fourier coefficients and bounds an integral identity by Schwarz's inequality, reaching an inequality that fails at $s=1/6$. The statement follows the paper's condition (1) and equation (3) (printed p. 185); the proof is not reconstructed in this repository. Atkinson later raised his own bound, to $1/3$ and then, in a 1969 paper, to $\pi/8$ for $n<1600$ and to a constant $s_0$ for all large $n$, as the introduction of Biró's 1994 paper records; the problem page records both papers and why neither has a claim page. Later full proofs with larger constants by another author are Biró 1994 and Biró 2000.

Acceptance. Refereed: the paper appeared in Acta Mathematica Academiae Scientiarum Hungaricae, a refereed journal, in volume 12, fascicles 1--2, whose title page prints 1961, so the paper dates itself 1961, as the site and the library card do; this page's date is the first day of that year, the issue month not being recorded. The publisher's record (Crossref, accessed 2026-10-07) carries a print date of March 1964 for the same article; that is the record's error and is disregarded. Reviewed: the site's curator, Thomas Bloom, labels the problem PROVED (LEAN) and credits this paper with the solution on erdosproblems.com/519 (page last edited 1 February 2026, accessed 2026-10-07), with the community database in agreement (its record of 2026-10-06 lists the problem as proved, as of its last update on 19 April 2026). Two Lean developments declare themselves formalizations of Atkinson's proof and are linked above: a file in Boris Alexeev's lean-proofs repository, which the formal-conjectures statement file (as of 2026-10-07) cites at that repository's main branch and which is linked here pinned to the revision of 24 June 2026, the latest to change the file as of 2026-10-07, whose header names Atkinson as the informal author and Aristotle and John Jennings as the formal authors and builds on Lean 4.29.1 with Mathlib, and the gist of 19 April 2026 that the thread post announcing the autoformalization by Aristotle links. The files' headers and theorem statements, give $z_1=1$, all $\lvert z_i\rvert\le1$ and the bound $1/6$; neither file has been built or audited in this repository, so they are links and not formalized evidence. No independent review is recorded here and none is claimed.

Depends on. Nothing in this wiki: the argument is the paper's own, and the normalization step is elementary and recorded on the library card.