---

Claim. Let $\epsilon_0,\epsilon_1,\dots$ be one sequence of independent uniform signs and $\nu_n(r)$ the number of zeros of $f_n(z)=\sum_{k\le n}\epsilon_kz^k$ in the closed disk of radius $r$, counted with multiplicity. Almost surely, uniformly for $x$ in compact sets,

$$\frac{\nu_n(1+x/n)}{n}\to\Phi(x)=\frac12\Bigl(1+\coth x-\frac1x\Bigr), \qquad\Phi(0)=\frac12,$$

and the case $x=0$ is the convergence $R_n/(n/2)\to1$ asked by Problem 522. The same laws are claimed for Steinhaus coefficients, for real and for complex Gaussian coefficients, and for bounded, centrally symmetric, nondegenerate coefficients; for signs the rate $\limsup_n(\log n)\lvert\nu_n(1)/n-1/2\rvert\le128$ almost surely. The preprint Almost-Sure Radial Laws for Nested Random Polynomials and Erdős Problem #522 by Sebastien Kawada was first released, with its formalization, as version 1.0.0 of the repository on 2026-09-25, and version 1.1.0 was deposited on Zenodo on 2026-09-26 (the record gives 2026-09-25 as its publication date); the claim was registered on the site's proof-claims tab on 2026-09-26 with Mantis Cartographer-1 named as the system used. The route starts from Jensen's formula, which expresses the count of zeros in a disk as a derivative in the radius of the mean of $\log\lvert f_n\rvert$ over the circle; for one fixed degree that mean is shown to lie close to $\log\sigma_n(r)-\gamma/2$ outside an event of probability decaying like a power of $n$, so Borel–Cantelli yields the law along the sparse sequence of degrees $n=j^8$. The degrees between two consecutive eighth powers are then handled by a stability argument: the coefficients appended to $f_{j^8}$ perturb it by a uniformly small amount, most zeros near the unit circle have a derivative that is not small, and Rouché's theorem tracks each such zero across the whole block of degrees. The author states that all main results are formally verified in Lean 4: the repository was released as version 1.0.0 on 2026-09-25 with the theorem Erdos522.erdos_522, said to have been completed on 2026-09-22, and a later revision proves the formal-conjectures statement of the problem with that catalog's own definitions.

Submission note. Posted to erdosproblems.com as a proof claim by Sebastien Kawada (account SebastienKawada) on 26 September 2026, giving "Mantis Cartographer-1" as the AI used:

Claim. Let ε_0, ε_1, ... be i.i.d. uniform ±1 and f_n(z) = Σ_{k≤n} ε_k z^k (one sequence, all n). Almost surely, (1/n)#{z : f_n(z) = 0, |z| ≤ 1 + x/n} → ½(1 + coth x − 1/x) uniformly for x in compact sets; x = 0 gives R_n/(n/2) → 1. The same holds for Steinhaus, real and complex Gaussian, and nondegenerate bounded symmetric coefficients. For ±1 coefficients, moreover, R_n = n/2 + O(n/log n) almost surely, with limsup (log n)|R_n/n − 1/2| ≤ 128. All of these results are formally verified in Lean. Proof idea. By Jensen's formula, radial counts are slopes of the angular average of log|f_n|, which at a fixed degree concentrates around log σ_n(r) − γ/2 with polynomially small failure probability; Borel–Cantelli gives the law along N = j^8. To reach every degree, we show that few zeros near the unit circle have a small derivative, and follow every other zero by Rouché's theorem to within o(1/N) for all n up to (j+1)^8, since the appended tails are uniformly small. Notes: I completed a Lean 4 proof of Erdős Problem #522, the theorem Erdos522.erdos_522 (for i.i.d. uniform ±1 coefficients, almost surely ν_n(1)/n → 1/2, where ν_n(1) counts the zeros of f_n(z) = ε_0 + ε_1 z + ⋯ + ε_n z^n in the closed unit disk), on 22 September 2026. The full formalization, release v1.0.0 (commit b3c1d7c), has been on GitHub since 18:54 UTC on 25 September, as its GitHub Actions run records. To my knowledge, this is the earliest formal proof of the problem. Paper: doi:10.5281/zenodo.22970145 (https://zenodo.org/records/22970145). Formalization: https://github.com/chreia/erdos-522.

Depends on. No page of this wiki.

Standing. Claimed. The community database recorded the repository as a Lean formalization on 2026-09-26, which set the site's label to OPEN (LEAN) while its informal status stays open pending human reading, and the formal-conjectures statement links two revisions of the repository as formal proofs since 2026-09-29; the catalog links, it does not referee. The claim has no comments on the tab, no human review is documented, and nothing was built, replayed or audited here, so the formalized evidence kind is not listed. Earlier informal proofs of the same statement are on Chojecki 2026 and Kwon–Zou 2026; an earlier Lean proof credited to Colin Snyder is on Snyder 2026, and an independent Lean proof of both coefficient readings is on Kitamura 2026.