Erdős Problem #522 (1961) resolved with a Lean-verified proof
Half the zeros of random ±1 polynomials lie in the unit disk, almost surely (Kawada, MIT CSAIL)
Awaiting review
The takeaway
A 1961 question of Erdős about the zeros of polynomials with random ±1 coefficients gets a formally verified answer, accepted against the statement in Google DeepMind’s Formal Conjectures. The author says he originated the mathematics; unnamed in-house models from MIT’s Kellis Lab helped with the Lean formalization and with checking derivations.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- 3 of 5
- Last verified
- 12 October 2026
Your AI and this story
- GPT-6 Astra161 days after its cutoff
- Claude Opus 5.5100 days after its cutoff
- Gemini 3.8 Flash191 days after its cutoff
- Grok 4.7130 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 100 days before it.
Key facts
- Paper: ‘Universal Radial Laws for Random Polynomials: Erdős Problem #522 and Non-Universal Fluctuations’, arXiv 2610.11324 [math.PR], 8 Oct 2026; Sebastien Kawada, MIT; 82 pages
- Problem (paper): ‘In 1961 Erdős asked whether ν_n(1)/n → 1/2 almost surely’, where ν_n(1) counts the zeros of f_n(z) = ε_0 + ε_1 z + … + ε_n z^n in the closed unit disk and the ε_k are independent random signs
- Earlier: Yakir proved the statement in probability (|ν_n(1) − n/2| < n^(9/10) with probability tending to one). Paper: ‘In April 2026, Chojecki and Kwon and Zou each posted an informal argument for the almost-sure statement for random signs.’
- Radial law: for bounded symmetric, real Gaussian or circular complex Gaussian coefficients, the proportion of zeros in the disk of radius 1 + x/n converges almost surely to ½(1 + coth x − 1/x), uniformly in x; so almost all zeros lie within O(1/n) of the unit circle
- Rate for random signs: almost-sure convergence at the unit circle at rate O(n^(−1/4) √(log n)), even with arbitrary dependence between degrees
- Fluctuations: the variance of the zero count is (c_G + κ_4/12)·n + O(n^(399/400)), depending on the coefficient law through its fourth cumulant; for random signs the constant is c_G − 1/6
- Verification: ‘Ours is the first formally verified proof of Erdős Problem #522. Its Lean formalization was completed on September 22, 2026.’ The repository lists 173 main theorems depending only on the axioms propext, Classical.choice and Quot.sound, and a single-file proof checkable in the Lean web editor
- Formal statement: the theorem proves Erdos522.erdos_522 as written in Google DeepMind’s Formal Conjectures project, whose maintainers reviewed the formal proof (acknowledgments)
Show 1 more
- AI disclosure (acknowledgments): ‘The Lean formalization and the checking and refinement of several derivations were aided by internal models developed in the Kellis Lab at MIT CSAIL, including language models, latent representation models, and graph neural networks acting on the dependency structure of the proof. The author originated the mathematical approach and established the results presented here.’
What happened
A Littlewood polynomial has every coefficient equal to +1 or −1. Pick the signs by coin flips and ask where the zeros fall: they cluster near the unit circle, and Erdős asked in 1961 whether exactly half of them, in the limit, lie inside or on it for almost every infinite sequence of flips. Convergence in probability was known. The almost-sure version needs control over all degrees at once, because each new coefficient moves every zero.
Kawada’s paper proves the almost-sure statement and describes the zeros at finer scales. Magnified by the degree n, their distance from the circle follows one fixed law for a wide class of coefficient distributions. The fluctuations of the count do depend on the distribution, through its fourth cumulant.
The whole development is formalized in Lean 4. The theorem matches the statement of Problem #522 that Google DeepMind’s Formal Conjectures project had written down in advance, which removes the usual doubt about whether a formal proof proves the intended claim. The paper says in-house models of the Kellis Lab at MIT helped with the formalization and with checking derivations, and that the mathematical approach is the author’s.
Why it matters
It is a named Erdős problem closed with a machine-checked proof against an independently written formal statement, days after erdosproblems.com froze proof claims and removed its open/solved labels (6 Oct). It also shows a different pattern from the autonomous results of autumn 2026: a human-led proof where AI did the formalization work, using a lab’s own models that the paper does not name or describe further.
What is disputed or not yet verified
| Verification | Lean 4 with Mathlib, kernel-replayed; accepted as a solution to the Formal Conjectures statement; unrefereed preprint |
|---|
The Lean project was not rebuilt for this entry, and erdosproblems.com/522 was not read (the site removed its open/solved status labels on 6 Oct). No expert reaction was found on 12 Oct 2026.
Sources
4 sources from 4 sites. Numbers match the chips in the text.
4 sources: 4 primary
Primary
- arXiv 2610.11324: Universal Radial Laws for Random Polynomials: Erdős Problem #522 and Non-Universal Fluctuationsarxiv.org, paper
- Lean formalization and paper repository (chreia/erdos-522)github.com, code
- Formal Conjectures: Erdos522.erdos_522google-deepmind.github.io, docs
- Erdős Problem #522 (erdosproblems.com)erdosproblems.com, docs
Changes
- Filed from the arXiv PDF and the repository README (found by a manual arXiv scan)