---

Claim. Let $p(a,q)$ be the least prime congruent to $a$ modulo $q$. The manuscript A Complete Candidate Proof of Erdős Problem 971 by KyungMin Han (revised 26 July 2026) states, as its main theorem, that there are absolute constants $c,C>0$ and $q_0$ such that for every $q\ge q_0$

$$\#\{a\bmod q:\ (a,q)=1,\ p(a,q)>(1+c)\,\phi(q)\log q\}\ \ge\ C\,\phi(q),$$

which is the question of Problem 971 answered yes. The author presents it as a candidate proof, unconditional except for the correctness of two cited published theorems, and asks for review by specialists.

Submission note. Posted to erdosproblems.com as a proof claim by KyungMin Han (account Dogcake) on 25 July 2026, giving "GPT 5.6 Pro" as the AI used:

For

$$R=\left\lfloor\frac{\phi(q)\log q}{q}\right\rfloor, \qquad X=qR, >$$

write

$$N_a(X)=\#\{p\le X:p\equiv a\pmod q\}, \quad > C_2=\sum_{(a,q)=1}\binom{N_a(X)}2, \quad C_3=\sum_{(a,q)=1}\binom{N_a(X)}3. >$$

The proposed analytic route is

$$V(X;q)\gg X\log q \quad\Longrightarrow\quad > C_2\gg\phi(q),$$

using the pointwise Friedlander-Goldston lower bound for

Hooley's variance, and

$$C_3\ll\phi(q),$$

using a uniform upper-bound sieve

for the three forms

$$p,\qquad p+rq,\qquad p+sq,$$

followed by a uniform

average of their singular series. At primes dividing 'q', the local factor is exactly '(1-1/ℓ)^{-2}', so the resulting '(q/φ(q))^2' factor is cancelled by the number of available shift pairs.

Argument, as the claimant describes it. Take the cutoff $X=qR$ with $R=\lfloor\phi(q)\log q/q\rfloor$, so that the primes up to $X$ number about $\phi(q)$, one per reduced class on average, and let $N_a(X)$ count the primes up to $X$ in the class $a$. The second factorial moment $\sum_a\binom{N_a(X)}{2}$ over reduced classes is bounded below by a constant times $\phi(q)$, from the pointwise lower bound of Friedlander and Goldston (1996) for Hooley's variance of primes in progressions; the third factorial moment $\sum_a\binom{N_a(X)}{3}$ is bounded above by a constant times $\phi(q)$, from an upper-bound sieve for the three linear forms $p$, $p+rq$, $p+sq$ (cited to an explicit prime-tuple bound of Dubbe, 2024) followed by an average of the singular series over the shift pairs, where the local factors at primes dividing $q$ produce a factor $(q/\phi(q))^2$ that the number of shift pairs cancels. The two moment bounds force a positive proportion of classes to hold at least two primes below $X$; since the total count of primes is $\phi(q)+o(\phi(q))$, a positive proportion of classes hold none; and the prime number theorem bounds the primes added when the cutoff grows to $(1+c)\phi(q)\log q$, so a positive proportion of empty classes survive. The author names the normalization and range of the variance bound, the uniformity of the three-form sieve and the singular-series average for smooth moduli as the steps most in need of checking.

Formalization. The Lean 4 file lean/Erdos971Forum.lean of the author's repository (Lean 4.27.0 with Mathlib, single file importing only Mathlib) proves the finite reduction and nothing analytic: the theorem prime_moment_method_to_least_prime_classes fixes one modulus $d$, two cutoffs $X_0\le X_1$ and real constants, and takes five hypotheses as parameters: a lower bound $\alpha\phi(d)$ for the second factorial moment at $X_0$, an upper bound $\beta\phi(d)$ for the third, an inequality among $\alpha$, $\beta$, $\delta$ and a truncation level (the moment method's gap condition), a total of at most $(1+\varepsilon)\phi(d)$ primes in reduced classes up to $X_0$, and at most $\eta\phi(d)$ primes added between the cutoffs. From these it concludes that at least $(\delta-\varepsilon-\eta)\phi(d)$ reduced classes modulo $d$ have least congruent prime beyond $X_1$; it also proves that a class holds no prime up to $X$ exactly when its least congruent prime exceeds $X$, using Mathlib's Dirichlet theorem. The companion AnalyticTargets.lean states the four analytic hypotheses as propositions, in eventual form in $d$ with $\varepsilon\to0$, without proving them; the gap condition is a check on the constants. The author's verification record reports a GitHub-hosted build with axiom closure propext, Classical.choice, Quot.sound for the three principal theorems and no sorry, and says plainly that this is a formal proof of the conditional finite implication and not of the analytic manuscript. The Lean file declares no sorry, axiom or native_decide; this corpus has not built it. The formalization does not reach the problem's statement, so it is not counted as evidence.

Postings. The proof claim was submitted to the site's proof-claims tab on 25 July 2026 by the forum account Dogcake, which posts as the author, naming KyungMin Han as the claimant and GPT 5.6 Pro as the AI system used. The claimant personally labeled the entry a partial proof claim. The manuscript's main theorem is the full statement and its title calls it a complete candidate proof, so the scope recorded here is full, following the manuscript over the claimant's own label. The repository was published the same day and revised on 26 July 2026, when the author wrote in the claim's thread, in the first person, that the PDF and Lean file had been revised and that the Lean development verifies only the finite reduction. The links above pin that revision, the repository's last commit(its 26 July 2026 status note records the author's attestation that the work was substantially assisted by the AI system and that they take responsibility for the mathematics). The repository carries no license. The site's claim entry links the write-up under the name Erdos971_candidate_verification_note.pdf; the revised PDF erdos971_candidate_proof.pdf is the same file in the pinned revision.

Standing. Claimed, with scope full on the manuscript's main theorem, against the claimant's own partial label. The site's label is OPEN; the tab's disclaimer says that a listing does not mean anyone associated with the site has examined the proof, and no review of the whole proof is recorded. The only other comment under the claim, of 28 September 2026, announces a separate Lean proof of the same statement by a different author along a related route, recorded on its own claim page; that comment credits priority to this claim and adds that its author checked that Theorem 2 of Friedlander and Goldston is pointwise in $q$ as this manuscript uses it, the variance step the author asked reviewers to examine; that is a check of one step, not a review of the whole proof. There is no refereed version and no acceptance by the site.

Depends on. No page of this wiki. The cited inputs, the Friedlander and Goldston variance bound and the prime-tuple upper bound, have no pages in this wiki.