{"id":"palomar/PALOMAR-2026-09-20-000008","url":"https://github.com/linrock/math-proofs/tree/1571a487465fb6a87f92dcc46f1bd71b0846c413/erdos-973","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-20-000008-v1.json","repo":"https://github.com/linrock/math-proofs","tags":["math.CV","math.NT","complex-analysis","number-theory","lean","erdos-problems"],"score":0,"title":"Erdős 973: power sums cannot all be exponentially small","trust":"high","domain":"math.CV","source":"palomar","authors":["Linmiao Xu"],"reviews":0,"subject":"math.CV","summary":"A complete Lean 4 proof of the negative answer to Erdős problem 973: power sums of complex numbers on or outside the unit circle cannot all be exponentially small. For each fixed C > 1 and all sufficiently large n, any n such numbers have some order 2 ≤ k ≤ n+1 with |∑_i z_i^k| > C^(-n), even without the original condition z₁ = 1. The proof follows the residual-polynomial method in Tan, Wang, Huang, and Chen’s August 2026 paper “Residual bounds for Schur-stable polynomials,” using a fixed-degree polynomial test. This submission provides a complete machine-checked proof of the negative answer…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-20","reactions":{},"formalized":true,"formalizes":[{"title":"Residual bounds for Schur-stable polynomials","identifier":"https://arxiv.org/abs/2608.02043v3","relationship":"formalizes"}]}