Erdős problem 428

Is there a set $A\subseteq \mathbb{N}$ such that, for infinitely many $n$ , all of $n-a$ are prime for all $a\in A$ with $0 < a < n$ and $\liminf\frac{\lvert A\cap [1,x]\rvert}{\pi(x)}>0?$

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

428.lean

Retained formal statement1 of 1

Is there a set $A\subseteq \mathbb{N}$ such that, for infinitely many $n$ , all of $n-a$ are prime for all $a\in A$ with $0 < a < n$ and $\liminf\frac{\lvert A\cap [1,x]\rvert}{\pi(x)}>0?$

FormalConjectures/ErdosProblems/428.leanErdos428.erdos_4284 linesExact file

1True ↔2  ∃ A,3    (∃ᶠ (n : ℕ) in Filter.atTop, ∀ a ∈ A, 0 < a → a < n → Nat.Prime (n - a)) ∧4      Filter.liminf (fun n => Erdos428.primeDensityRatio A n) Filter.atTop > 0

OpenStatement only, no proof