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
Are there infinitely many primitive weird numbers?
sorry ↔ Set.Infinite Erdos470.PrimitiveWeirdOpenStatement only, no proof