---

Claim. The Lean 4 theorem Erdos521.erdos_521_negative in the lean-proofs repository states, in the repository's index, that it is not almost surely true that $R_n/\log n\to2/\pi$ for the distinct real roots of a random $\{-1,1\}$ polynomial, which is the negative answer to Problem 521 for that reading. The index credits the proof to Colin Snyder (starfleetmath.com) and records that the repository's continuous integration builds the file against a pinned Mathlib and checks that the headline theorem uses no sorry and no axiom beyond propext, Classical.choice and Quot.sound. The files were hosted in the repository on 2026-07-23, the date this page carries, and the formal-conjectures statement of the problem has linked the file at the repository's revision of 2026-07-30 as its formal proof since 2026-08-07 (the record link is pinned at the catalog's commit of that day), marking the problem solved with answer false; the catalog's docstring says the result was first obtained by others, who deserve the credit, and that the link is to an independent machine-checked proof. The imports of the development name a cone criterion, records, the Kochen–Stone lemma and a fourth-moment analysis, so its route appears related to the cone-record arguments of the other claims.

Depends on. No page of this wiki.

Standing. Claimed. This corpus has not built, replayed or audited the development, no write-up accompanies it, and the catalog's tag links a proof without refereeing it; the hosting repository's verdicts file records a term-by-term faithfulness read by its maintainers (521: faithful, the negation proved through an event of positive measure) beside its CI build and axiom check, and says neither replaces peer review; this corpus has not examined the statement's fidelity. The site labels the problem OPEN (page last edited 19 October 2025). The written arguments for the same conclusion are on Kovač 2026, Kwon–Zou 2026, Sneiderman 2026 and An–Lin 2026; a second Lean development, in Boris Alexeev's repository, is on Alexeev 2026.