DISPROVED (LEAN), the site's label. Enrique Barschkis, posting as ebarschkis, constructed a measurable set of positive measure and an interval of $x$ on which infinitely many $n$ put $nx$ outside every $r\cdot E$, by varying the Buczolich–Mauldin construction; the accepted claim is Barschkis's counterexample, credited by the site's curator and not refereed. The Lean proofs behind the site's qualification are linked on the claim page; none was built here.