PROVED (LEAN): Alexeev, Putterman, Sawhney, Sellke and Valiant [APSSV26] showed that $\{\alpha p_n\}$ is not well-distributed for every real $\alpha$, the accepted claim Alexeev, Putterman, Sawhney, Sellke and Valiant 2026, accepted on the site's label and Terence Tao's thread comment; no journal version of the preprint was found on 2026-10-07. The site's Lean qualification refers to a formalization that takes the Banks–Freiberg–Turnage-Butterbaugh theorem [BFT15] as an axiom; a later public development in Boris Alexeev's repository states an unconditional proof of the same statement; neither is built or audited here, so the claim page lists no formalized evidence. Champagne, Lê, Liu and Wooley [CLLW24] had earlier found one irrational $\alpha$ with this property, the partial claim Champagne, Lê, Liu and Wooley 2024.