Benkoski and Erdős [BeEr74](https://mathscinet.ams.org/mathscinet/relay-station?mr=347726) proved that the set of weird numbers has positive density.

Erdős problem 470

Benkoski and Erdős BeEr74 proved that the set of weird numbers has positive density.

The source's own material, retained exactly.

8 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

470.lean

Retained formal statement5 of 8

Liddy and Riedl LiRi18 have shown that an odd weird number must have at least 6 prime divisors.

FormalConjectures/ErdosProblems/470.leanErdos470.erdos_470.variants.odd_weird_prime_div1 lineExact file

1∀ (n : ℕ), Odd n → n.Weird → 6 ≤ {m | m ∈ n.divisors ∧ Nat.Prime m}.ncard

SolvedStatement only, no proof