Erdős problem 1209
Let be a sequence of integers which tends to infinity sufficiently fast. If there is an such that all are primes then must there exist infinitely many such ?
Sources
FormalConjectures/ErdosProblems/
1209.lean
Retained formal statement
What if we ask for to be squarefree instead of prime?
A similar construction provides a counterexample to the squarefree question.
False ↔ ∃ f, ∀ (a : ℕ → ℕ), StrictMono a → (∀ (k : ℕ), f k ≤ a k) → (∃ n, ∀ (k : ℕ), Squarefree (n + a k)) → {n | ∀ (k : ℕ), Squarefree (n + a k)}.InfiniteSolvedStatement only, no proof