Erdős 973: power sums cannot all be exponentially small
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-20-000008
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-20-000008/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-20-000008/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'