Erdős problem 1141 · problems.science

Are there infinitely many $n$ such that $n-k^2$ is prime for all $k$ with $(n,k)=1$ and $k^2 < n$ ?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1141.lean

Retained formal statement1 of 1

Are there infinitely many $n$ such that $n-k^2$ is prime for all $k$ with $(n,k)=1$ and $k^2 < n$ ?

In [Va99] it is asked whether $968$ is the largest integer with this property, but this is an error, since for example $968-9=7\cdot 137$ .

The list of $n$ satisfying the given property is [A214583] in the OEIS. The largest known such $n$ is $1722$ .

The answer is negative: [APSSV26b] proves a stronger finiteness theorem, deducing it from Pollack [Po17]. Oriike [Or26] formalised the deduction in Lean.

FormalConjectures/ErdosProblems/1141.leanErdos1141.erdos_11411 lineExact file

1False ↔ Infinite ↑{n | Erdos1141.Erdos1141Prop n}

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