Skip to content

Erdős problem 429

Is it true that, if A⊆NA\subseteq \mathbb{N} is sparse enough and does not cover all residue classes modulo pp for any prime pp, then there exists some nn such that n+an+a is prime for all a∈Aa\in A?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

429.lean

Retained formal statement1 of 1

Is it true that, if A⊆NA\subseteq \mathbb{N} is sparse enough and does not cover all residue classes modulo pp for any prime pp, then there exists some nn such that n+an+a is prime for all a∈Aa\in A?

Weisenberg [We24] has shown the answer is no: AA can be arbitrarily sparse and missing at least one residue class modulo every prime pp, and yet A+nA+n is not contained in the primes for any n∈Zn\in \mathbb{Z}. (Weisenberg gives several constructions of such an AA.)

FormalConjectures/ErdosProblems/429.leanErdos429.erdos_4297 linesExact file
False ↔  ∃ f,    Filter.Tendsto f Filter.atTop Filter.atTop ∧      ∀ (A : Set ℕ),        A.Infinite →          (∀ (N : ℕ), (A ∩ Set.Icc 1 N).ncard ≤ f N) →            (∀ (p : ℕ), Nat.Prime p → ∃ b, ∀ a ∈ A, ↑a ≠ b) → ∃ n, ∀ a ∈ A, Nat.Prime (n + a)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.