---

Claim. The repository daizisheng/erdos-971-lean, at the commit of 28 September 2026 linked above, proves Erdos971.erdos_971 : Erdos971Statement, where Erdos971Statement is copied from the formal-conjectures file for the problem with its open answer fixed to true: there are reals $c>0$ and $C>0$ such that for all large $d$ at least $C\,\phi(d)$ residues $a<d$ coprime to $d$ have least prime $p(a,d)>(1+c)\,\phi(d)\log d$, with $p(a,d)$ the least prime congruent to $a$ modulo $d$. This is the question of Problem 971 answered yes. The author announced the development in the site's proof-claims thread on 28 September 2026, in a comment under Han's claim of July 2026, saying that it follows the same second- and third-moment skeleton with the variance step replaced by a correlation between primes and rough numbers, in the manner of Section 8 of Friedlander and Goldston's 1996 paper, that the proof route was found with an AI system (GPT-6) and formalized with another (Claude), and that the priority is Han's.

Formalization, as the repository describes it. The README states that the main theorem has axiom closure propext, Classical.choice, Quot.sound, that no sorry remains and that the project declares no axiom; that the prime number theorem, the asymptotic for the logarithmic integral and Mertens' product come from the public PrimeNumberTheoremAnd project, the Bombieri--Vinogradov theorem from a public repository that formalizes it, and the fundamental lemma of sieve theory is proved inside the repository by a blocked Bonferroni sieve; and that everything, dependencies included, is compiled from source and kernel-checked, with leanchecker replaying the project's own modules. The toolchain is Lean 4.33.1 with Mathlib v4.33.1; separately, a patch script repairs an inconsistent pin in the dependency chain by vendoring ten files of the PrimeNumberTheoremAnd fork. The README's own status line is "complete, no project axioms, no sorry; unreviewed", and it says that what must be taken on trust is the Lean kernel and the fidelity of the five-line copied statement. The repository's history, ten commits on 28 September 2026, moves from a skeleton with axioms for the analytic inputs to a version with none. This corpus has not built, replayed or audited the development, so formalized is not listed.

Standing. Claimed. The site's label is OPEN, the development is not on the site's proof-claims tab as an entry of its own, and the formal-conjectures file on its main branch tagged the statement research open with a sorry body on 2026-10-07. No review is recorded, and the author's README says the same. The repository is under the Apache-2.0 license.

Depends on. No page of this wiki. The public Lean developments the proof imports are not pages here.