---

Claim. For one infinite sequence of independent coefficients uniform on $\{-1,1\}$, and separately for coefficients uniform on $\{0,1\}$, the number $R_n$ of roots of $\epsilon_0+\epsilon_1z+\dots+\epsilon_nz^n$ in the closed unit disk, counted with multiplicity, satisfies $R_n/(n/2)\to1$ almost surely, simultaneously for all degrees. The first statement answers Problem 522 in the affirmative; the second settles the $\{0,1\}$ reading that the site records as a possible intent of Erdős. Kenta Kitamura's Lean 4 development, public on 2026-09-25, imports the formal-conjectures statement file and proves its two theorems Erdos522.erdos_522 and Erdos522.erdos_522.variants.zero_one with the answer true, using that catalog's definitions; a standalone file for the Lean web editor is also provided. The author's comment on the site's discussion thread (2026-09-26) reports that both proof files compile and that #print axioms for both final theorems lists only propext, Classical.choice and Quot.sound, and discloses that the exploration, proofs, documentation and comment were produced with assistance from ChatGPT and OpenAI Codex using GPT-6 Astra, and from Claude Code using Claude Opus 5.5. The README says the route was chosen to be light for formalization, using no Berry–Esseen theorem, log-Sobolev or Pisier inequality or small-ball estimate from the literature, and proves only the qualitative limit; it credits the informal proofs of the $\{-1,1\}$ statement by Chojecki and by Kwon and Zou and says no earlier proof of the $\{0,1\}$ statement is known to the author. The README carries an AI-generated mathematical explanation outlining the proof (Jensen's formula at three radii, smoothing, a martingale concentration bound on the cube and a Lindeberg comparison); no separate manuscript accompanies the development.

Depends on. No page of this wiki.

Standing. Claimed. The formal-conjectures catalog merged the author's pull request on 2026-09-28 and has tagged both statements research solved with links to this development since then; the catalog links, it does not referee. No proof claim was registered on the site's proof-claims tab, no human review is documented, and nothing was built, replayed or audited here, so the formalized evidence kind is not listed. 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 informal proofs are on Chojecki 2026 and Kwon–Zou 2026; an earlier Lean proof of the $\{-1,1\}$ statement, credited to Colin Snyder, is on Snyder 2026.