Problem
erdos:932{r | 2 ≤ {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}.Infinite
Matching claims
No direct claims
This problem has no directly related claim record.