VibeMathedMath problems solved with AI
Sign in

Improved maximal prime-gap lower bound

Let G(X)G(X) denote the largest gap between consecutive primes not exceeding XX, and let log⁡j\log_j denote the jj-fold iterated logarithm. The paper proves that, for all sufficiently large XX,G(X)≫log⁡X (log⁡2X)2 log⁡4X(log⁡3X)2. G(X)\gg \frac{\log X\,(\log_2 X)^2\,\log_4 X}{(\log_3 X)^2}. Equivalently, there is an absolute constant c>0c>0 such that G(X)G(X) is at least cc times the quantity above for all sufficiently large XX. This improves Rankin's classical lower bound by a factor of log⁡2X\log_2 X.

Result
Proved(see note)
Status
Partial result
AI contribution
AI-discovered
Method
Argument
Field
Analytic number theory
Posed by
Paul Erdős
Year posed
1955
Years open
71y
Solved
2026-09-03
Model
GPT 6 Astra
Vendor
OpenAI
Collaborators
—
Verification
Site-confirmed
Publication
Preprint
Significance
60 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

The paper provesG(X)≫log⁡X (log⁡2X)2 log⁡4X(log⁡3X)2 G(X)\gg \frac{\log X\,(\log_2 X)^2\,\log_4 X}{(\log_3 X)^2} for all sufficiently large XX. Its main new ingredient is a short-translates theorem: for any sufficiently small set S⊆[1,H]S\subseteq[1,H] with ∣S∣≤δx|S|\le\delta x, one can find a short translate making every corresponding linear form composite. Combining this with an Erdős--Rankin covering argument produces prime-free intervals of the claimed length. This directly and asymptotically improves the August 2026 GPT-5.6 Sol boundG(X)≫log⁡Xlog⁡2Xlog⁡4X G(X)\gg\frac{\log X\log_2 X}{\log_4 X} by the unbounded factorlog⁡2X(log⁡4X)2(log⁡3X)2. \frac{\log_2 X(\log_4 X)^2}{(\log_3 X)^2}.

What the AI did

The paper explicitly attributes the proof to GPT 6 Astra. The new argument introduces a short-translates proposition that allows a sparse residual set of positions to be made composite simultaneously. Its main construction uses specially chosen divisor-sum factors, a shared truncation of their product, and a nonnegative squared weight. The resulting proposition is then inserted into an Erdős--Rankin construction to obtain the improved maximal prime-gap bound.

Verification

Site-confirmed on 4 September 2026: this site built openai/LongGapsBetweenPrimes at commit 03a1190d from a clean checkout on GitHub Actions (run 33843996072). lake build completed all 8707 jobs, the build's own #print axioms line reads 'LongGapsBetweenPrimes.long_prime_gaps' depends on axioms: [propext, Classical.choice, Quot.sound], and leanchecker replayed the library through the kernel. The statement was read by hand: Challenge.lean asserts, for some c > 0 and all sufficiently large X, a consecutive prime gap below X exceeding c times log X (log_2 X)^2 log_4 X / (log_3 X)^2, which is the claimed bound and not a weaker cousin of it. What remains is what a kernel cannot see: there is no human author, and no named mathematician has commented yet.

Sources

Submitted by VibeGene on

Changelog2 changes

Discussion