Skip to content

Erdős problem 428

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

428.lean

Retained formal statement1 of 1

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

FormalConjectures/ErdosProblems/428.leanErdos428.erdos_4284 linesExact file
TrueA,    (∃ᶠ (n : ℕ) in Filter.atTop, ∀ aA, 0 < aa < nNat.Prime (n - a)) ∧      Filter.liminf (fun n => Erdos428.primeDensityRatio A n) Filter.atTop > 0
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page