Erdős Problem a Daythe open tracker

Erdős Problem #1141

DISPROVED LEANdatabase updated 2026-04-11

The statement as posed is false. A solution has also been checked by machine, in Lean.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

The cutoff \(m^{1/4 + \varepsilon}\) of Theorem 1.3 of [Po17].

The primes \(\ell \leq m^{1/4+\varepsilon}\) with \(\chi(\ell) = 1\). This does not require \(\chi\) to be quadratic. That hypothesis belongs to the theorem below, as it does in the paper.

The property that \(n-k^2\) is prime for all \(k\) with \((n,k)=1\) and \(k^2 < 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.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/1141.
Prizenone
Topicsnumber theory, primes
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA214583
Original pageerdosproblems.com/1141
NOBODY HAS SENT US AN ATTEMPT YET

If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.