---

Claim. The Lean 4 theorem Erdos522.erdos_522 in the lean-proofs repository of williamjblair proves the proposition Erdos522Claim of the repository's statement file for the problem: on every probability space carrying a sequence of measurable, independent, fair Boolean coordinates, read as the signs $\pm1$, almost surely $R_n/(n/2)\to1$, where $R_n$ counts the roots of $\sum_{k\le n}\epsilon_kz^k$ in the closed unit disk with multiplicity. This is the affirmative answer to Problem 522 for $\{-1,1\}$ coefficients. The repository's index credits the proof to Colin Snyder (starfleetmath.com), names the statement file and the theorem, and records that the repository's continuous integration builds the file and prints the axioms of the headline theorem, reporting them clean; it also names the formal-conjectures statement file as the development's target, but the catalog's file for the problem does not link it (as of the catalog's revision of 2026-09-29). The files were hosted in the repository on 2026-07-23, the date this page carries, by a commit titled as the host's verification of the Star Fleet proof. The proof file amalgamates some twenty research modules in about 16,700 lines, whose section names mention sparse frequency matrices, van der Corput estimates, circle-parameter measures, radial weights and moment bounds for cosine products, and the final theorem is derived from a moment bound for radial cosine sums. No write-up accompanies the development, and no thread post or proof claim on the site announces it.

Depends on. No page of this wiki.

Standing. Claimed. Nothing was built, replayed or audited here, the axiom check is the repository's own report, and the repository's index marks the statement faithful (faithful: true) beside its CI build and axiom check, with no verdict note for 522 in its verdicts file; this corpus has not examined its fidelity. The site's label records a Lean formalization of the separate Kawada 2026 claim and no human acceptance (OPEN (LEAN); page last edited 06 December 2025). The other full claims are Chojecki 2026, Kwon–Zou 2026, Kawada 2026 and Kitamura 2026.