Problem 521

../

claims/: The 6 claim pages of Problem 521, one per claimant's result; the problem's standing derives from them.

---

Statement. Let $(\epsilon_k)_{k\geq 0}$ be independently uniformly chosen at random from $\{-1,1\}$. If $R_n$ counts the number of real roots of $f_n(z)=\sum_{0\leq k\leq n}\epsilon_k z^k$ then is it true that, almost surely,

$$\lim_{n\to \infty}\frac{R_n}{\log n}=\frac{2}{\pi}?$$

Formulation. The site's Statement draws the coefficients from $\{-1,1\}$. Its commentary records that Erdős's source [Er61, p. 252] is ambiguous between $\{-1,1\}$ and $\{0,1\}$, the constant being $1/\pi$ in the second case. In the site's discussion on 7 September 2025 the curator wrote that Erdős "was most likely intending to ask whether, if $\epsilon_k\in\{-1,1\}$ is an infinite sequence chosen uniformly at random, and $R_n(f)$ counts the number of real roots of $\sum_{0\leq k\leq n}\epsilon_k z^k$, then $\lim_{n\to\infty} R_n(f)/((2/\pi)\log n)=1$", that the curator was "minded to keep the problem as it's written here" with the caveat that it is not strictly a problem of Erdős, and, after Tao read the source's binary-digit construction as $\{0,1\}$-valued, that the curator was "leaning towards Erdős intending $\{-1,1\}$ as the explanation that implies fewer mistakes on his part". The Statement is therefore the site's wording unchanged, the reading the curator adopted; no Statement (precise) is needed, since the wording already fixes $\{-1,1\}$. The $\{0,1\}$ version, where the constant would be $1/\pi$ and which has no claim, is a variant and does not enter the standing. Under the Statement the answer is no: almost surely $R_n/\log n$ has lower limit $1/\pi$ and upper limit at least $2/\pi$, so it does not converge to $2/\pi$ (Alexeev 2026, accepted on the Lean build). The site's label OPEN (page last edited 19 October 2025) reflects that neither claim on its proof-claims tab has been reviewed, not a different reading of the question.

Status. Disproved. The site labels the problem OPEN as of 2026-10-06 (page last edited 19 October 2025), which reflects that neither of the two claims on its proof-claims tab has been reviewed, not a different reading of the question. The tab carries two full proof claims, both disproofs, with no comments and no acceptance, and the site's remarks cite [EO56], [Er61] and [Do24]. The derived standing is solved/disproved for the Statement, through the Lean development with Codex as formal author on Alexeev 2026, which this corpus built and audited: almost surely $R_n/\log n$ has lower limit $1/\pi$ and upper limit at least $2/\pi$, so it does not converge almost surely to $2/\pi$. Five further full claims of the negative answer remain pending, none refereed or independently reviewed: the working note on Kovač 2026 (generated by ChatGPT 5.5 Pro, posted on the thread on 2026-04-30), with the lower limit at most $1/\pi$ on an event of positive probability; the note on Kwon–Zou 2026; the Lean development on Snyder 2026, which the formal-conjectures catalog links as a formal disproof and which proves the negation alone; and the two claims on the tab, Sneiderman 2026 and An–Lin 2026. Kwon–Zou, Sneiderman and An–Lin claim the lower limit $1/\pi$ almost surely.

Source. erdosproblems.com/521, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #521, https://www.erdosproblems.com/521.

References.

• [Do24] Y. Do, A strong law of large numbers for real roots of random polynomials. arXiv:2403.06353 (2024).
• [EO56] Erdős, Paul and Offord, A. C., On the number of real roots of a random algebraic equation. Proc. London Math. Soc. (3) (1956), 139-160.
• [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254.

Formalization. Statement in formal-conjectures (pinned at the file's last change, 2026-09-18), tagged research solved with answer false since 2026-08-07, linking the Star Fleet Math Lean proof recorded on Snyder 2026; the catalog links, it does not referee, and this corpus has neither built nor audited that proof. A second Lean development, in Boris Alexeev's lean-proofs repository with Codex as its formal author, which the catalog does not link, was built and audited by this corpus: its declarations Erdos521.erdos521_oscillation and Erdos521.not_erdos_521 use only propext, Classical.choice and Quot.sound and match the repository's comparator challenge, as Alexeev 2026 records.

Current assessment

The question, as the site states it, asks whether $R_n/\log n\to2/\pi$ almost surely for one infinite sequence of independent uniform signs, where $R_n$ counts the real roots of the degree-$n$ partial polynomial. The site records that the source [Er61, p. 252] is ambiguous between $\{-1,1\}$ and $\{0,1\}$ coefficients, the constant being $1/\pi$ in the second case; the thread's discussion of September 2025 between the site's curator and Tao found the literal text to use binary digits while the section's other problems use signs. The site's Statement is the $\{-1,1\}$ version, its commentary notes the $\{0,1\}$ alternative, and the curator leans towards $\{-1,1\}$. Every claim recorded here addresses the $\{-1,1\}$ reading; the $\{0,1\}$ variant has no claim. What is known: Erdős and Offord [EO56] give $(2/\pi+o(1))\log n$ real roots with high probability, and Do [Do24] proves the strong law $R_n[-1,1]/\log n\to1/\pi$ for the roots in $[-1,1]$. Comments of September 2025 observed that the available concentration bounds give only polynomial tails, too weak for an almost-sure statement, and suggested the law might fail. In April 2026 the thread developed a disproof strategy: Letwin's Gaussian-process limit of the rescaled polynomial near the endpoints of $[-1,1]$, Tao's buckets, and Kovač's suggestion to look for degrees with no real root outside $[-1,1]$. Every claim follows that route: infinitely many degrees have no exterior real root (a cone or record event of the walk built from the reversed coefficients, with positive probability in the first note and almost surely in the three later notes and the Alexeev development, while Snyder's Lean theorem proves only the negation), so the lower limit is $1/\pi$ by Do's law, while convergence in probability keeps the upper limit at least $2/\pi$. A note posted by Kovač on 2026-04-25 claims to settle the same question for standard Gaussian coefficients, which is a question of Pritsker rather than this problem. On the thread for Problem 522 (21 April 2026) Letwin wrote that Letwin's own solutions include this problem and that Michelen and Yakir have a stronger result implying Problem 522; no manuscript was found. The claims differ in rigor and in authorship: two are AI-generated notes posted by their prompters, two are Lean developments without a write-up (one credited to Snyder, one with Codex as formal author in Alexeev's repository), and of the two on the tab, Sneiderman's describes itself as a synthesis of earlier arguments while An and Lin's is self-contained. None has been checked by a named reader on the thread. The Lean development in Alexeev's repository, which this corpus built and audited, proves the lower limit $1/\pi$ and the upper limit at least $2/\pi$ almost surely, so the problem is disproved; the written notes and Snyder's development have not been examined here, and the $\{0,1\}$ variant, which does not enter the standing, remains open.

Search scope: the site's problem page as exported (last edited 19 October 2025), its discussion thread (20 comments) and proof-claims tab (accessed 2026-10-07), the community database entry (open), the formal-conjectures file and the index entry of the pinned Lean proof, Boris Alexeev's lean-proofs repository, the GitHub repositories and notes linked from the thread, and an arXiv author search for Letwin (no paper on this problem); no OpenAI release item names this problem. MathSciNet and zbMATH were not searched and X was not used.

Known Results

• [EO56]: for $\pm1$ coefficients, $R_n=(2/\pi+o(1))\log n$ with probability tending to one; this is convergence in probability, not the almost-sure law asked here.
• [Do24]: for one infinite sequence of signs, almost surely $R_n[-1,1]/\log n\to1/\pi$ for the roots in $[-1,1]$; the roots outside $[-1,1]$ depend on the last coefficients and are not covered.
• Accepted on a Lean build here: Alexeev 2026, a Lean development with Codex as formal author, proves that for $\{-1,1\}$ coefficients, almost surely, $R_n/\log n$ has lower limit $1/\pi$ and upper limit at least $2/\pi$, counting distinct real roots, so the almost-sure law fails.
• Claimed, not accepted: $R_n/\log n$ does not converge almost surely, with lower limit $1/\pi$ (and upper limit at least $2/\pi$) for $\{-1,1\}$ coefficients, on Kovač 2026 (positive probability of the lower limit, by a cone-record criterion), Kwon–Zou 2026 (almost surely, by a Lévy zero–one argument), Sneiderman 2026 (almost surely, by a finite-prefix restart), An–Lin 2026 (almost surely infinitely many even degrees with no exterior root, by a reflected random walk), and Snyder 2026 (a Lean theorem, linked by formal-conjectures).
• Claimed variant, not this problem: for standard Gaussian coefficients the almost-sure law is claimed to fail with positive probability of a lower limit at most $1/\pi+\delta$, in the AI-generated note of 2026-04-25 recorded on the Kovač page, which answers a question posed at the 2019 AIM workshop on random polynomials; unreviewed.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

• erdos_1961_unsolved_problems
• do_2024_strong_law_large_numbers_real_roots
• do_2024_strong_law_large_numbers_real_roots / lemma_2_3
• do_2024_strong_law_large_numbers_real_roots / theorem_1_1
• erdos_1956_number_real_roots_random_algebraic_equation
• erdos_1956_number_real_roots_random_algebraic_equation / theorem