ERDŐS ASKED IN 1961. HALF, ALMOST SURELY

Toss a coin for each coefficient of a polynomial: heads gives +1, tails gives −1. The result is a random Littlewood polynomial, 1 ± z ± z² ± … ± zⁿ. Like any polynomial of degree n, it has n roots — points of the complex plane where it equals zero.

In 1961, the mathematician Erdős asked where those roots go. More precisely: as the degree grows, does the fraction of roots lying inside the closed unit disk — the circle of radius 1 and everything within — tend to exactly one half, with probability one? The question became Problem #522 in the list of Erdős problems. A weaker version, true “with high probability” rather than “almost surely”, had been proved earlier by Yakir.

Sebastien Kawada of MIT now answers Erdős’s question: yes.

Hugging the circle

The paper proves more than the one-half. Almost all the roots crowd into a thin band around the unit circle, at a distance of order 1/n. Zoom in on that band with the variable x = n(|z| − 1), and the share of roots inside the circle of radius 1 + x/n settles on a single curve:

Φ(x) = ½ (1 + coth x − 1/x)

At x = 0, the curve gives exactly ½: Erdős’s answer. The same curve holds for a whole family of random coefficients — coin flips, random points on a circle, Gaussian numbers. That is the universal part of the title.

The result even holds when the polynomials of different degrees are linked in any way at all: built by adding one coin toss at a time, or drawn completely afresh at each degree. For coin flips, the excess of roots inside the disk over n/2 stays below roughly n^(3/4).

Where universality stops

The paper then looks at the small fluctuations around one half. Here the coefficients’ law starts to matter. For Gaussian coefficients, the variance of the excess grows like 0.3059 × n. For other symmetric laws, it shifts by one twelfth of a quantity called the fourth cumulant, which measures how heavy the tails of the law are. For coin flips, the constant becomes 0.3059 − 1/6. Computer experiments on 16,384 random polynomials of degree up to one million agree with these predictions.

How it is proved

Two classical tools do the heavy lifting. Jensen’s formula turns a count of roots in a disk into an average of the logarithm of the polynomial around a circle; that average turns out to concentrate tightly. The hard step is to go from a sparse sequence of degrees to every degree at once. For the fluctuations, the argument principle turns the excess of roots into a signed count of how often a curve, drawn by the polynomial on the unit circle, crosses a line.

Checked by machine

Every main result of the 82-page paper is formally verified in the Lean 4 proof assistant. The proof of Problem #522 was accepted as a solution to its formal statement in Google DeepMind’s Formal Conjectures project, and a single file lets anyone replay it in a web browser. The author writes that internal AI models from Manolis Kellis’s lab at MIT, including language models, helped with the Lean formalisation and with checking several derivations; the author states that the mathematical approach is their own.

In April 2026, two informal arguments for the same statement were posted on the Erdős problems forum. Kawada says this proof and its approach are original, and that it is the first formally verified one. Sixty-five years after the question was asked, the machine-checked answer reads: half, almost surely.