Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 971
claims/: The 3 claim pages of Problem 971, one per claimant's result; the problem's standing derives from them.
Statement. Let be the least prime congruent to . Does there exist a constant such that, for all large ,
for many values of ?
Status. OPEN on erdosproblems.com; two full proof claims are pending. The
site's proof-claims tab carries one entry: KyungMin Han's candidate proof of
25 July 2026, made with GPT 5.6 Pro, that a positive proportion of reduced
classes have least prime beyond for all large , by a
second- and third-moment count of primes in classes, with a Lean file covering
only the finite reduction
(claim page); the
claimant, posting as the forum account Dogcake, labeled the entry a partial
proof claim, while the manuscript's main theorem is the full statement, and
the full scope recorded here follows the manuscript. A comment under that
entry of 28 September 2026 announces Shisheng Li's Lean 4 development proving
the formal-conjectures statement of the problem along a related route, found
with GPT-6 and formalized with Claude by its author's account, with no sorry
and the standard three axioms by the same account, not built or audited by
this corpus
(claim page). The
tab's disclaimer says that a listing does not mean anyone associated with the
site has examined the proof; no review of either proof is recorded beyond Li's
check of one step of Han's argument, recorded on Han's claim page; this page
records the claims without adopting them. The site's commentary credits Erdős
[Er49c] with the assertion along an infinite sequence of moduli
(claim page,
accepted, partial). The discussion thread holds no proof: a comment of 31
January 2026 derives the answer yes from a uniform prime-tuple hypothesis by a
Poisson count of primes per class, and two others give heuristics and a
literature note on the larger quantity .
Source. erdosproblems.com/971, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #971, https://www.erdosproblems.com/971.
References.
- [Er49c] Erdős, P., On some applications of Brun's method. Acta Univ. Szeged. Sect. Sci. Math. (1949), 57-63 (claim page).
Formalization. Statement in formal-conjectures.
Progress
Not yet compiled.
Known Results
Not yet compiled.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.