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
Fang [Fa22](https://arxiv.org/abs/2207.12906) has shown there are no odd weird numbers below .
∀ n < 10 ^ 21, Odd n → ¬n.WeirdSolvedStatement only, no proof