---

Claim. For every strictly increasing sequence of primes $q_0<q_1<\cdots$ with non-decreasing gaps, $\liminf_n q_n/n^2\ge M/(\Lambda+G)>0.864289$, where $M=3\cdot5\cdot7\cdot11\cdot13\cdot17=255255$, $\Lambda=295318$ and $G=17.2244\ldots$ is an explicit series over the primes at least $19$; in eventual form, $q_n>0.864289\,n^2$ for all large $n$. Richter's bound $0.352$ (1976) follows as a corollary, in the exact form of the formal-conjectures statement erdos_455.variants.liminf.

Covers. The lower bound $\liminf q_n/n^2>0.864289$ and, as a corollary, Richter's bound. The limit question of Problem 455, whether $q_n/n^2\to\infty$, is not addressed.

Method, as the development describes it. A run of equal gaps $d$ is an arithmetic progression of primes, which has at most $P(d)-2$ terms after its first outside a sparse exceptional set, $P(d)$ the least prime not dividing $d$; eventually all terms are coprime to $M$, which turns the counting of gaps into a max-plus dynamic program on the $92160$ units of $\mathbb Z/M\mathbb Z$, periodic in the gap value. An integer potential on the units certifies that the program gains at most $\Lambda$ per period. The certificate, a computation of about $5\cdot10^{10}$ elementary operations, is checked by the Lean kernel without native_decide: the values are packed into eight natural numbers with $17017$ fields of $9$ bits each, so that every step of the value iteration is a few dozen big-integer operations whose soundness is proved once. The development states that its main results use only the axioms propext, Classical.choice and Quot.sound.

Claimant. Yongxi Lin, the repository's author and maintainer. Its metadata states that the mathematics of the underlying draft (an unpublished note of 26 September 2026, not included in the repository) and the Lean development were produced by AI under Lin's direction, naming Claude for the draft and Claude Opus 5.5 through Claude Code for the formalization, and that no AI system is listed as an author; the review recorded there is by the formalizing agents, with no human review. The result was not posted to the site's proof-claims tab under Lin's name. A claim posted to that tab on 5 October 2026 by the user satorunet, whose headline bound was Lin's $0.8642$, was withdrawn and replaced the next day by a claim crediting Lin and extending the method by one prime, the sibling page satorunet.

Standing. Claimed. The site's label is OPEN (page last edited 7 October 2025), and its commentary records only Richter's bound. The Lean development was not built or audited here, so no formalized evidence is listed, and nothing outside the repository records acceptance.

Depends on. No page of this wiki.