---

Schinzel [Sc87] proves the conjecture of Rényi, first published by Erdős, that the least number $Q_k$ of nonzero coefficients of the square of a polynomial with exactly $k$ nonzero complex coefficients tends to infinity with $k$, in the explicit form

$$Q_k > \frac{\log\log k}{\log 2}.$$

The bound is the case $l=2$ of his Theorem 1: for a field $K$, a polynomial $f\in K[x]$ with $T\ge2$ terms whose power $f^l$ has $t$ terms, and either $\operatorname{char}K=0$ or $\operatorname{char}K>l\deg f$,

$$t \ge l+1+\frac{1}{\log 2}\log\Bigl(1+\frac{\log(T-1)}{l\log 4l-\log l}\Bigr).$$

The problem's $f(k)$ is the same minimum taken over rational polynomials only, so $f(k)\ge Q_k$ and $f(k)\to\infty$, which answers Problem 485 yes. The proof inducts on $t$, using Hajós's lemma on the number of terms forced by a zero of high multiplicity, a reduction of $f^l\in K[x^d]$ to $f\in K[x^d]$, and a sequence of differential operators; the source card digests the paper, whose Theorem 2 treats positive characteristic. Schinzel notes that the bound is far from Erdős's upper bound $Q_k<C_1k^{1-C_2}$ (card). The paper was received by the journal on 1985-11-22, as its last page records, and published in 1987.

Depends on. Nothing in this wiki; the result rests on the refereed paper linked above.

Acceptance. Refereed: the paper appeared in Acta Arithmetica 49 (1987), no. 1, 55–70. Reviewed: the site's curator, Thomas F. Bloom, records the problem as solved by Schinzel with this bound in the problem's commentary (page last edited 2026-04-08, read 2026-10-07), and Schinzel and Zannier's refereed sharpening of 2009 (Schinzel and Zannier 2009) builds on the theorem. Formalization: a Lean 4 file in the lean-proofs repository, linked above at its pinned commit, declares itself a formalization of Schinzel's solution, names Codex and GPT-5.6 Sol as its formal authors under Lean v4.33.0 and Mathlib v4.33.0, and proves erdos_485, that the minimum over rational polynomials tends to infinity, from a quantitative theorem schinzel_support_bound for the square case in an imported development; the file ends with an axiom print. The site labels the problem PROVED, with no Lean qualification, and the formal-conjectures statement file for the problem points to that proof. This corpus has neither built the development nor audited its statement, so no formalized evidence is listed.