Erdős problem 470
Benkoski and Erdős [BeEr74](https://mathscinet.ams.org/mathscinet/relay-station?mr=347726) proved that the set of weird numbers has positive density.
Sources
FormalConjectures/ErdosProblems/
470.lean
Retained formal statement
The smallest weird number is 70.
(∀ n < 70, ¬n.Weird) ∧ Nat.Weird 70TextbookStatement only, no proof