Erdős problem 470
Benkoski and Erdős BeEr74 proved that the set of weird numbers has positive density.
Sources
FormalConjectures/ErdosProblems/
470.lean
Retained formal statement
Melfi Me15 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