---

Claim. Let $G(X)$ be the largest gap between consecutive primes not exceeding $X$ and $\log_k$ the $k$-fold iterated logarithm. There is an absolute constant $c>0$ such that, for all sufficiently large $X$,

$$G(X)\ge c\,\frac{\log X\,(\log_2X)^2\log_4X}{(\log_3X)^2}.$$

This is Theorem 1.1 of the note Improved Long Gaps Between Primes, published by OpenAI on 3 September 2026, the day of the GPT-6 Astra launch post that links it (the note itself prints no date), with the author line "OpenAI" and the sentence that the proof is due to GPT 6 Astra. Its main input, Proposition 1.2, is a statement about short translates: there is an absolute $0<\delta<1/2$ such that for all large $x$, with $Q$ the product of the primes up to $x$, any set $S$ of at most $\delta x$ integers in an interval $[1,H]$ with $x<H\le x(\log x)^2$, and any residue $0\le b<Q$, some $1\le t\le e^x$ makes every $b+Qt+s$ with $s\in S$ composite. The note improves Rankin's 1938 bound by a factor $\log_2X$ and is a $\log_2X$ gain over the question of Problem 4, which it therefore answers in the affirmative for every $C$; its introduction cites, as its reference [13] (an argument by GPT 5.6 Sol posted on the site), the 2026 bound of DottedCalculator's manuscript, which gains a factor $(\log_3X)^2/(\log_4X)^2$ over the same question, but states its own gain only against Rankin's bound; Theorem 1.1 exceeds the DottedCalculator bound by a factor $\log_2X(\log_4X)^2/(\log_3X)^2$, and the submitter writes in the thread that they do not know how to combine the two improvements. The weight is a squared truncated divisor sum over auxiliary primes with coefficients proportional to a reciprocal logarithm, chosen so that the weighted expected number of forms without a prime factor in the auxiliary range is below one. Boris Alexeev filed the claim on the site's proof-claims tab on 4 September 2026; the claimant is the organization, and an abridged chain of thought accompanies the note. The basis of this page is the note's statements and proof outline.

Submission note. Posted to erdosproblems.com as a proof claim by OpenAI (account BorisAlexeev) on 4 September 2026, giving "GPT-6 Astra" as the AI used:

As part of the GPT-6 Astra launch, OpenAI announced that Astra had given an improvement to the longest gap between primes by roughly a $\log \log n$ factor. (It's $\log \log n$ over the Rankin bound in the original question.) The main input is the following statement about translates of a set of integers: There is an absolute constant $0 < \delta < 1/2$ such that the following holds for all sufficiently large $x$. Let $x < H \le x(\log x)^2$, let $Q = \prod_{p\le x} p$, and let $S \subseteq [1, H] \cap \mathbb{Z}$ have cardinality $k \le \delta x$. For every integer $0 \le b < Q$, there is an integer $1 \le t \le e^x$ such that $b + Qt + s$ is composite for every $s \in S$. An abridged chain of thought is also available.

Standing. The site's commentary, last edited before this claim was filed, does not record the bound; the thread's three comments ask how the argument relates to the Rankin method and whether it can be combined with the other improvements, and no reviewer independent of the claimant has endorsed it. The note has no refereed publication. The claim therefore stays claimed.

Formalization. The linked repository, pinned at the commit in the link, describes itself as a Lean 4 formalization of the note's results: its metadata names the note as the source, lists OpenAI as author, reports zero sorry and the axioms propext, Classical.choice and Quot.sound for the declarations long_prime_gaps, long_gap_theorem and short_translates, and records that the formalization was produced by GPT 6 Astra under Codex with later human refinement and is self-assessed. The file Challenge.lean states long_prime_gaps in indexed form with a sorry as a comparator reference, and LongGapsBetweenPrimes.lean (4,546 lines) proves it and contains no sorry, axiom or native_decide token. This corpus has not built or kernel-checked the development, so its self-reported build awards nothing here.

Depends on. Nothing beyond the cited note.