---

Claim. For one infinite sequence of independent uniform signs, with $R_n$ the number of distinct real roots of $f_n(x)=\sum_{k\le n}\epsilon_kx^k$, almost surely

$$\liminf_{n\to\infty}\frac{R_n}{\log n}=\frac{1}{\pi},\qquad \limsup_{n\to\infty}\frac{R_n}{\log n}\ge\frac{2}{\pi},$$

so $R_n/\log n$ does not converge almost surely to $2/\pi$ and Problem 521 has a negative answer for the $\{-1,1\}$ reading. The file Erdos521.lean in Boris Alexeev's lean-proofs repository, added on 2026-08-26 and linked above at the repository's commit, presents itself as an unconditional disproof of the problem for one infinite sequence of symmetric signs, counting distinct real roots, and names Codex as its formal author. It states Erdos521.not_erdos521 (with the alias Erdos521.not_erdos_521), the negation of the almost-sure convergence conjecture, and Erdos521.erdos521_oscillation, the almost-sure lower and upper limits above with extended-real limits. Its docstring says the proof establishes the interior-root strong law, an Abel cone criterion, a harmonic cone-survival bound, a record second-moment bound and a finite-prefix zero-one upgrade, that infinitely many degrees with no exterior real root give the lower limit while coefficient reversal and convergence in measure give the upper limit, and that every input is proved within the development, with no assumption of Do's theorem or of the notes it lists. Those informal sources are Erdős (the statement), An and Lin (the oscillation claim), the working note of 2026-04-29, Section 7 (cone records), Sneiderman (the finite-prefix restart), Do (the interior-root strong-law strategy) and Can–Nguyen (local root and sign-grid estimates). The file ends with #print axioms commands whose recorded output is propext, Classical.choice and Quot.sound.

Depends on. No page of this wiki: the development proves its inputs rather than assuming the results of the notes it lists.

Acceptance. Formalized. This corpus's verification built the repository's src/latest project at the commit linked above (Lean v4.33.0, Mathlib v4.33.0), a later revision of the development posted on 2026-08-26. The top file Erdos521.lean and the module Erdos521/Model.lean, which holds the definitions the challenge pins, are unchanged since that posting, but proofs in the supporting modules were repaired and reformatted on 2026-09-04 and 2026-09-05, so the acceptance rests on the revision at the linked commit. The verification checked the axioms of Erdos521.erdos521_oscillation and Erdos521.not_erdos_521, which are exactly propext, Classical.choice and Quot.sound. The repository's comparator challenge ComparatorChallenges/ErdosProblems/Erdos521.lean pins both declarations with the definitions their types reach (the polynomial $\sum_{k=0}^n\epsilon_kx^k$, its set of distinct real roots and their count, the normalized count $R_n/\log n$, the fair-sign law, the infinite product of that law and the conjecture), and the fingerprint of each declaration was found identical to the challenge. The statement was audited clause by clause against the problem's Statement: the signs are one infinite sequence drawn from the product of fair Bernoulli laws on $\{1,-1\}$, $f_n$ uses $\epsilon_0$ to $\epsilon_n$, roots are counted without multiplicity, as the formal-conjectures statement also counts them, Erdos521.not_erdos_521 is exactly the negative answer, and Erdos521.erdos521_oscillation gives the lower limit $1/\pi$ and the upper limit at least $2/\pi$ almost surely, taken in the extended reals. The acceptance covers the $\{-1,1\}$ reading of the Statement; the $\{0,1\}$ reading the site also keeps is outside it. Not reviewed: no write-up accompanies the development, neither the formal-conjectures catalog, which links the Lean development on Snyder 2026, nor the site's proof-claims tab nor the community database records it, and the site labels the problem OPEN (page last edited 19 October 2025). Not refereed: no journal version exists. The written arguments for the same conclusion are on Kovač 2026, Kwon–Zou 2026, Sneiderman 2026 and An–Lin 2026; the first, third and fourth are among the development's informal sources, and their claims stay pending on their own pages.