Erdős Problem 973 asks whether there is a constant C>1 such that points z_j with |z_j|>=1 (and z_1=1) can make max_{2<=k<=n+1}|sum z_j^k| smaller than C^{-n}. The question was recorded as open.

The proof argues by contradiction. It writes F(t)=prod(1-z_j t) as an exponential times a coefficient-small perturbation and uses the resulting coefficient identities to bound the normalized first power sum. It then shows overconvergence of truncated exponentials on an open disk outside the unit disk. Finally, Montel's theorem and the identity theorem show that a Cauchy transform cannot converge to a nonzero constant there. A Lean 4 development accompanies the paper, with its verification extent given by the declarations and remaining axioms in the repository.

For every λ>0 and all sufficiently large n, the maximum exceeds e^{-λn}. So the nth root of the optimal maximum tends to 1, and no constant C>1 exists, which answers Erdős 973 negatively.