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 $(1+c)\phi(d)\log d$ for all large $d$, by a second- and third-moment count of primes in classes, with a Lean file covering only the finite reduction (claim page (Han, 2026)); 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 (Li, 2026)). 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 (Erdős, 1949), 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 $\max_ap(a,d)$.