Erdős Problem 932

Reference: erdosproblems.com/932

theorem erdos_932 : {r : ℕ | 2 ≤ (Finset.filter (fun (m : ℕ) => m.maxPrimeFac < Nat.nth Nat.Prime r.succ - Nat.nth Nat.Prime r) (Finset.Ioo (Nat.nth Nat.Prime r) (Nat.nth Nat.Prime r.succ))).card}.Infinite

Let $p_k$ denote the $k$th prime. For infinitely many $r$ there are at least two integers $p_r < n < p_{r+1}$ all of whose prime factors are $< p_{r + 1} - p_r$.

theorem erdos_932.variants.one_le : {r : ℕ | 1 ≤ (Finset.filter (fun (m : ℕ) => m.maxPrimeFac < Nat.nth Nat.Prime r.succ - Nat.nth Nat.Prime r) (Finset.Ioo (Nat.nth Nat.Prime r) (Nat.nth Nat.Prime r.succ))).card}.HasDensity 0

Erdős could show that the density of $r$ such that at least one such $n$ exist is $0$.