Aftermath bot: New page: long gaps between primes (OpenAI preprint and Lean repository), with Radomskii and LeanPool

2026-10-15T01:53:53Z

New page: long gaps between primes (OpenAI preprint and Lean repository), with Radomskii and LeanPool

New page

'''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'' (log2 ''X'')2 log4 ''X'' / (log3 ''X'')2. 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'' (log2 ''X'')2 log4 ''X'' / (log3 ''X'')2 (Theorem 1.1). The preprint states that this improves Rankin's bound by a factor log2 ''X'' and that the proof is due to GPT 6 Astra. Source: the preprint [https://cdn.openai.com/pdf/51126fac-1b68-4128-9666-c908bcc16033/long_gaps.pdf 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'')2 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.''' [https://github.com/openai/LongGapsBetweenPrimes 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 <code>formalization.yaml</code> records a "full formalization of main results", no <code>sorry</code>, and only the axioms <code>propext</code>, <code>Classical.choice</code> and <code>Quot.sound</code>, for the Comparator statement <code>long_prime_gaps</code> and for <code>long_gap_theorem</code> and <code>short_translates</code>. 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'' log2 ''X'' / (log3 ''X'')2, and Rankin improved this to ''G''(''X'') ≫ log ''X'' log2 ''X'' log4 ''X'' / (log3 ''X'')2. 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'' log2 ''X'' log4 ''X'' / log3 ''X''. The preprint also cites an argument by GPT 5.6 Sol, posted on the Erdős Problems website, giving ''G''(''X'') ≫ log ''X'' log2 ''X'' / log4 ''X''.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 15 October 2026)
|-
| 2026-10-07 (v1), 2026-10-09 (v2) || [https://arxiv.org/abs/2610.10762 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''2 + 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 || [https://github.com/LeanPool/lean-pool LeanPool] (GitHub; project card <code>LeanPool/projects/long-gaps-between-primes.yaml</code>) || Formal (repository import) || Lists the formalization, imported from commit <code>03a1190</code> 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.

[[Category:OpenAI results]]

Long gaps between primes - Revision history

Aftermath bot: New page: long gaps between primes (OpenAI preprint and Lean repository), with Radomskii and LeanPool