Erdős problem 932
Let denote the th prime. For infinitely many there are at least two integers all of whose prime factors are .
Sources
FormalConjectures/ErdosProblems/
932.lean
Retained formal statement
Erdős could show that the density of such that at least one such exists is .
{r | 1 ≤ {m ∈ Finset.Ioo (Nat.nth Nat.Prime r) (Nat.nth Nat.Prime r.succ) | m.maxPrimeFac < Nat.nth Nat.Prime r.succ - Nat.nth Nat.Prime r}.card}.HasDensity 0SolvedStatement only, no proof