Erdős Problem 470

Reference: erdosproblems.com/470

def Erdos470.PrimitiveWeird (n : ℕ) : Prop

Primitive weird numbers are weird numbers such that no proper divisor of $n$ are weird.

Equations

• Erdos470.PrimitiveWeird n = (n.Weird ∧ ∀ d ∈ n.properDivisors, ¬d.Weird)

def Erdos470.AbundancyIndex (n : ℕ) : ℚ

The abundancy index is the sum of the divisors of $n$ divided by $n$.

Equations

• Erdos470.AbundancyIndex n = ↑(∑ d ∈ n.divisors, d) / ↑n

theorem Erdos470.erdos_470.part1 : (∃ (n : ℕ), n.Weird ∧ Odd n) ↔ sorry

Are there any odd weird numbers?

theorem Erdos470.erdos_470.part2 : Set.Infinite PrimitiveWeird ↔ sorry

Are there infinitely many primitive weird numbers?

theorem Erdos470.erdos_470.variants.weird_pos_density : {n : ℕ | n.Weird}.HasPosDensity

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

theorem Erdos470.erdos_470.variants.smallest_weird_eq_70 : (∀ n < 70, ¬n.Weird) ∧ Nat.Weird 70

The smallest weird number is 70.

theorem Erdos470.erdos_470.variants.prime_gap_imp_inf_prim_weird : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(primeGap n) < √↑(Nat.nth Nat.Prime n) / 10 → Set.Infinite PrimitiveWeird

Melfi Me15 has proved that there are infinitely many primitive weird numbers, conditional on the fact that $p_{n+1} - p_n < \frac{1}{10} p_n^{1/2}$ for all large $n$, which in turn would follow from well-known conjectures concerning prime gaps.

theorem Erdos470.erdos_470.variants.odd_weird_10_pow_21 (n : ℕ) : n < 10 ^ 21 → Odd n → ¬n.Weird

Fang Fa22 has shown there are no odd weird numbers below $10^21$.

theorem Erdos470.erdos_470.variants.odd_weird_prime_div (n : ℕ) : Odd n → n.Weird → 6 ≤ {m : ℕ | m ∈ n.divisors ∧ Nat.Prime m}.ncard

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

theorem Erdos470.erdos_470.variants.abundancy_index : (∀ (n : ℕ), n.Weird → ¬Odd n) → ∀ (n : ℕ), n.Weird → AbundancyIndex n < 4

If there are no odd weird numbers then every weird number has abundancy index < 4.