Erdős problem 1209 · problems.science

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$ ?

Sources

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

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1209.lean

Retained formal statement3 of 6

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.

FormalConjectures/ErdosProblems/1209.leanErdos1209.erdos_1209.parts.iii.a1 lineExact file

1False ↔ ∃ n, ∀ (k : ℕ), Nat.Prime (n + 2 ^ 2 ^ k)

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.

Sources

Search problems.science