Erdős Problem 1141

References:

• erdosproblems.com/1141
• A214583
• [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).

def Erdos1141.Erdos1141Prop (n : ℕ) : Prop

The property that $n-k^2$ is prime for all $k$ with $(n,k)=1$ and $k^2 < n$.

Equations

• Erdos1141.Erdos1141Prop n = ∀ (k : ℕ), k ^ 2 < n → n.Coprime k → Nat.Prime (n - k ^ 2)

instance Erdos1141.instDecidableErdos1141Prop (n : ℕ) : Decidable (Erdos1141Prop n)

Equations

• Erdos1141.instDecidableErdos1141Prop n = decidable_of_iff (∀ k ≤ (n - 1).sqrt, n.Coprime k → Nat.Prime (n - k ^ 2)) ⋯

theorem Erdos1141.erdos_1141 : sorry ↔ Infinite ↑{n : ℕ | Erdos1141Prop n}

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