Erdős Problem 428

Reference: erdosproblems.com/428

noncomputable def Erdos428.primeDensityRatio (A : Set ℕ) (n : ℕ) : ℝ

The density ratio of set $A$ up to $n$ relative to the prime counting function $\pi(n)$.

Equations

• Erdos428.primeDensityRatio A n = ↑(A ∩ Set.Icc 1 n).ncard / ↑n.primeCounting

theorem Erdos428.erdos_428 : sorry ↔ ∃ (A : Set ℕ), (∃ᶠ (n : ℕ) in Filter.atTop, ∀ a ∈ A, 0 < a → a < n → Nat.Prime (n - a)) ∧ Filter.liminf (fun (n : ℕ) => primeDensityRatio A n) Filter.atTop > 0

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?]