Long gaps between primes

Long gaps between primes is the subject of an OpenAI preprint, Improved Long Gaps Between Primes, published outside the openai/math collection together with a Lean 4 formalization. Write G(X) for the largest gap between consecutive primes not exceeding X, and log_j for the j-fold iterated logarithm. The preprint claims G(X) ≫ log X (log₂ X)² log₄ X / (log₃ X)². This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

The original result

Claim. There is an absolute constant c > 0 such that, for all sufficiently large X, G(X) ≥ c log X (log₂ X)² log₄ X / (log₃ X)² (Theorem 1.1). The preprint states that this improves Rankin's bound by a factor log₂ X and that the proof is due to GPT 6 Astra. Source: the preprint Improved Long Gaps Between Primes (OpenAI), hosted in the same folder as the preprint described on Bounded gaps between primes; an abridged chain of thought is published alongside it.
Method, as summarized in the preprint. The main input is a statement about short translates (Proposition 1.2): for x < H ≤ x(log x)² and a set S ⊆ [1, H] of at most δx integers, some translate b + Q(x)t + S with 1 ≤ t ≤ e^x consists entirely of composite numbers, where Q(x) is the product of the primes up to x. The proof uses the square of a truncated product of divisor sums as a weight, with a cutoff that the preprint compares to the simplex restriction in the Maynard–Tao sieve. Theorem 1.1 then follows by a modification of the Erdős–Rankin construction.
Formalization, as described by the repository. openai/LongGapsBetweenPrimes (commits of 2 and 3 September 2026; Lean 4.33.0 with mathlib) states in its README that it contains a Lean 4 formalization of the results, and the preprint states that the repository contains a complete Lean proof of Theorem 1.1. Its formalization.yaml records a "full formalization of main results", no sorry, and only the axioms propext, Classical.choice and Quot.sound, for the Comparator statement long_prime_gaps and for long_gap_theorem and short_translates. The same file describes an agent run with GPT 6 Astra in Codex followed by human-in-the-loop refinement, and gives the review status as "self-assessed". The Comparator configuration enables the nanoda checker.

Earlier published results

As recounted in the preprint: Westzynthius proved G(X)/log X → ∞; Erdős obtained G(X) ≫ log X log₂ X / (log₃ X)², and Rankin improved this to G(X) ≫ log X log₂ X log₄ X / (log₃ X)². Erdős asked whether the constant in Rankin's bound could be made arbitrarily large, offering a prize; this was proved independently by Maynard and by Ford, Green, Konyagin and Tao, whose joint work with Maynard gave G(X) ≫ log X log₂ X log₄ X / log₃ X. The preprint also cites an argument by GPT 5.6 Sol, posted on the Erdős Problems website, giving G(X) ≫ log X log₂ X / log₄ X.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 15 October 2026)
2026-10-07 (v1), 2026-10-09 (v2)	arXiv:2610.10762 (v1, v2), A. Radomskii; titled Long intervals of consecutive composite values of polynomials	Use (adaptation of the method)	For an irreducible integer-valued polynomial f of positive degree with positive leading coefficient, for every sufficiently large X the half-open interval from X/2 to X contains at least c_f log X log log X consecutive integers n with f(n) composite; the abstract states that this replaces the small fixed power of log log X in the earlier result of Ford and Gabdullin by the full factor, and that it applies to f(t) = t² + 1. The paper states that it adapts the short-translate construction of the OpenAI preprint to polynomial values.	arXiv v2.
2026-10-08 or earlier	LeanPool (GitHub; project card `LeanPool/projects/long-gaps-between-primes.yaml`)	Formal (repository import)	Lists the formalization, imported from commit `03a1190` of the OpenAI repository, with status "verified" and the three main declarations.	Project card in the LeanPool registry.

Notes

The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.