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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/1141.lean

Formal Conjectures

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.

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

AI collaborating with humans
Erdős AI contributions wiki · 25 Jan, 2026
Machine
GPT-5.2 Pro, GPT-5.2 Thinking
People
Quanyu Tang
Open the source record
Formalization
Erdős AI contributions wiki · 11 Apr, 2026
Machine
GPT-5.4 Pro
Open the source record
AI standalone
Erdős AI contributions wiki · 9 Apr, 2026
Machine
OpenAI internal model
Open the source record
construction
VibeMathed
Machine
OpenAI internal model
People
Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, Gregory Valiant
Reported outcome
resolved
Open the source record