Erdős problem 429
Is it true that, if is sparse enough and does not cover all residue classes modulo for any prime , then there exists some such that is prime for all ?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/429.leanFalse ↔ ∃ 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)Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:429 - PLBY Lean proofs
ErdosProblems.Erdos429
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine