Erdős Problem 1209

References:

• erdosproblems.com/429
• erdosproblems.com/1102
• erdosproblems.com/1209
• [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.

theorem Erdos1209.erdos_1209.parts.i : False ↔ ∃ (f : ℕ → ℕ), ∀ (a : ℕ → ℕ), StrictMono a → (∀ (k : ℕ), f k ≤ a k) → (∃ (n : ℕ), ∀ (k : ℕ), Nat.Prime (n + a k)) → {n : ℕ | ∀ (k : ℕ), Nat.Prime (n + a k)}.Infinite

Let $A=\{a_1<a_2<\cdots\}$ be a sequence of integers which tends to infinity sufficiently fast. If there is an $n$ such that all $n+a_k$ are primes then must there exist infinitely many such $n$?

Erdős [Er80] wrote 'unless I overlook a trivial way of getting a counterexample these questions are quite hopeless'. There is indeed a trivial counterexample (a variant of the construction in [erdosproblems.com/429]): define $a_1=2$ and for $k\geq 2$ let $a_k>a_{k-1}$ be a prime such that $a_k+k\equiv 0\pmod{q_k}$, where $q_k$ is some prime not dividing $k$. This sequence can be made to grow arbitrarily fast

See also [erdosproblems.com/429] and [erdosproblems.com/1102].

theorem Erdos1209.erdos_1209.parts.ii : False ↔ ∃ (f : ℕ → ℕ), ∀ (a : ℕ → ℕ), StrictMono a → (∀ (k : ℕ), f k ≤ a k) → (∃ (n : ℕ), ∀ (k : ℕ), Squarefree (n + a k)) → {n : ℕ | ∀ (k : ℕ), Squarefree (n + a k)}.Infinite

What if we ask for $n+a_k$ to be squarefree instead of prime?

A similar construction provides a counterexample to the squarefree question.

theorem Erdos1209.erdos_1209.parts.iii.a : False ↔ ∃ (n : ℕ), ∀ (k : ℕ), Nat.Prime (n + 2 ^ 2 ^ k)

Are there $n$ such that $n+2^{2^k}$ is always a prime?

ebarschkis and GPT have proved that there are no $n$ such that $n+2^{2^k}$ is always prime: let $n\geq 3$ be any odd integer. If $k$ is chosen sufficiently large, and $p=n+2^{2^{k}}$ is prime, then the multiplicative order of $2^{2^k}\pmod{p}$, say $m$ is odd, and hence if $l$ is chosen such that $2^l\equiv 1\pmod{m}$ then $p\mid n+2^{2^{k+rl}}$ for all $r\geq 1$.

This was formalized in Lean by Barschkis using ChatGPT.

theorem Erdos1209.erdos_1209.parts.iii.b : sorry ↔ ∃ (n : ℕ), ∀ (k : ℕ), Squarefree (n + 2 ^ 2 ^ k)

Are there $n$ such that $n+2^{2^k}$ is always squarefree?

theorem Erdos1209.erdos_1209.parts.iii.c : sorry ↔ ∃ (n : ℕ), {k : ℕ | Nat.Prime (n + 2 ^ 2 ^ k)}.Infinite

Are there $n$ such that $n+2^{2^k}$ is infinitely often a prime?

theorem Erdos1209.erdos_1209.parts.iii.d : sorry ↔ ∃ (n : ℕ), {k : ℕ | Squarefree (n + 2 ^ 2 ^ k)}.Infinite

Are there $n$ such that $n+2^{2^k}$ is infinitely often squarefree?