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
Melfi [Me15](https://mathscinet.ams.org/mathscinet/relay-station?mr=3276337) has proved that there are infinitely many primitive weird numbers, conditional on the fact that for all large , which in turn would follow from well-known conjectures concerning prime gaps.
(∀ᶠ (n : ℕ) in Filter.atTop, ↑(primeGap n) < √↑(Nat.nth Nat.Prime n) / 10) → Set.Infinite Erdos470.PrimitiveWeirdSolvedStatement only, no proof