Negative answer to Erdős Problem 521. The faithful Mathlib statement Claim is the proposed almost-sure convergence of the distinct real-root count of iid Rademacher polynomials to 2/pi after division by log n. Lean proves Erdos521.erdos_521_negative : ¬ Claim.

Authoritative verifier:
  ./verified_math/F-123_erdos-521-negative/verify.sh
Observed output (exit 0):
  Build completed successfully (3770 jobs).
  Erdos521.erdos_521_negative : ¬Erdos521.Claim
  depends on axioms: [propext, Classical.choice, Quot.sound]

The verifier compares the attached final proof closure to active sources, rejects sorry/admit/axiom throughout Research/, builds Research.Erdos521, checks the exact theorem type, and audits axioms. Statement fidelity is documented in check_answer/README.md; the final technical proof and dependency ledger are in F-123 and verified_math.md.
