Erdős Problem 1141

References:

• erdosproblems.com/1141
• A214583
• [APSSV26b] B. Alexeev, M. Putterman, M. Sawhney, M. Sellke, and G. Valiant, Short proofs in combinatorics, probability and number theory II. arXiv:2604.06609 (2026).
• [Or26] Y. Oriike, Lean formalisation of Erdős problem 1141 (2026)
• [Po17] P. Pollack, Bounds for the first several prime character nonresidues. Proc. Amer. Math. Soc. (2017), 2815--2826.
• [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 : False ↔ 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$.

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