Erdős problem 428
Is there a set such that, for infinitely many , all of are prime for all with and
Sources
FormalConjectures/ErdosProblems/
428.lean
Retained formal statement
Is there a set such that, for infinitely many , all of are prime for all with and
True ↔ ∃ A, (∃ᶠ (n : ℕ) in Filter.atTop, ∀ a ∈ A, 0 < a → a < n → Nat.Prime (n - a)) ∧ Filter.liminf (fun n => Erdos428.primeDensityRatio A n) Filter.atTop > 0OpenStatement only, no proof