VibeMathedMath problems solved with AI
Sign in

A tilted residue-class construction for long prime-free intervals

How large can the gap between consecutive primes be, infinitely often? Writing log⁡k\log_k for the kk-fold iterated logarithm, Erdős asked (problem #4, a $10,000 prize) whether pn+1−pn≫Clog⁡nlog⁡2nlog⁡4n/(log⁡3n)2p_{n+1}-p_n \gg C\log n\log_2 n\log_4 n/(\log_3 n)^2 for every CC; that was settled in 2016, and the record bound since has been Ford-Green-Konyagin-Maynard-Tao's pn+1−pn≫log⁡nlog⁡2nlog⁡4n/log⁡3np_{n+1}-p_n \gg \log n\log_2 n\log_4 n/\log_3 n. This work claims a stronger bound, G(T)≫log⁡Tlog⁡2T/log⁡4TG(T)\gg \log T\log_2 T/\log_4 T, an improvement by a factor of log⁡3T/(log⁡4T)2\log_3 T/(\log_4 T)^2, together with Y(X)≫Xlog⁡X/log⁡3XY(X)\gg X\log X/\log_3 X for the covering problem behind it.

Result
Proved(see note)
Status
Partial result
AI contribution
AI-discovered
Method
Argument
Field
Analytic number theory; large gaps between primes
Posed by
Paul Erdős
Year posed
1955
Years open
71y
Solved
2026-08-25
Model
GPT 5.6 Sol
Vendor
OpenAI
Collaborators
DottedCalculator (prompting and submission), Boris Alexeev (Lean formalisation)
Verification
Independently expert-verified
Publication
Announced
Significance
60 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Claims G(T)≫log⁡Tlog⁡2T/log⁡4TG(T)\gg\log T\log_2 T/\log_4 T against FGKMT's log⁡Tlog⁡2Tlog⁡4T/log⁡3T\log T\log_2 T\log_4 T/\log_3 T, a gain of log⁡3T/(log⁡4T)2\log_3 T/(\log_4 T)^2, together with Y(X)≫Xlog⁡X/log⁡3XY(X)\gg X\log X/\log_3 X for the covering problem behind it.

Ben Green resists calling it incremental: "The sieving procedure is different to the Erdos-Rankin one which underpinned all bounds on the problem since 1938, and it wins log⁡3N\log_3 N over that procedure. The [FGKMT] paper also wins a log⁡3N\log_3 N. These wins are essentially independent of one another so one now wins basically (log⁡3N)2(\log_3 N)^2 over Rankin's 1938 bound." He adds that the new sieve "by itself could have claimed the Erdos 10000 dollars for this question".

What is new is narrow: only the intermediate sieve is replaced, its hard cutoff smoothed into a probabilistic tilt; the hypergraph covering theorem and Maynard weight come from FGKMT. Readers on the thread note that several later sections reproduce FGKMT with no new content, and Green calls the exposition "horrific".

What the AI did

The paper has no human author. Its title block reads \author{GPT 5.6 Sol} and the PDF metadata records the same, with no acknowledgements section and no human contributor named anywhere in the manuscript.

The human in the loop is the pseudonymous submitter DottedCalculator, who prompted the model and whose own account of that role is unusually direct: "I am not familiar with sieve theory. The first draft was much shorter (19 pages) but I couldn't understand the sieve theoretical jargons and there were a few small steps missing that I had a really hard time with. I asked for all of the details self-contained to make checking the argument easier." So the human contribution was prompting, iteration and a request for self-contained detail - explicitly not the mathematics. Ben Green notes the contributor "seems to wish to stay anonymous".

One attribution discrepancy, recorded rather than smoothed over: the manuscript and its filename say GPT 5.6 Sol, while the erdosproblems.com claim was filed as "GPT 5.6 Pro (using GPT 5.6 Pro)" and the discussion refers throughout to ChatGPT 5.6 Pro.

Boris Alexeev's Lean development is downstream and formal - it transcribes the manuscript rather than producing it.

Verification

Expert-verified, by an unusually well-placed expert: Ben Green, a co-author of the FGKMT bound this beats, so a reader with every incentive to be sceptical rather than generous.

On 26 August he called it "an important claim" that "survives an initial plausibility check", while warning that "the exposition is truly horrible" and that verifying it would take time. On 27 August, after "a few hours thought and some conversations with Terry Tao and James Maynard", he wrote that he "became more or less convinced this is correct", adding that "a lean formalisation exists so we know it's correct, and experts closest to the area basically understand informally what the key ideas are and why the proof works". Boris Alexeev, who formalised it, states that the result is "formalized unconditionally in Lean".

That matches the audit done here on 30 August: 403 Lean files, 56,614 lines, no sorry\texttt{sorry}, no admit\texttt{admit}, no native_decide\texttt{native\_decide} and not one declared axiom, with the terminal theorem stated in primitive Mathlib terms and carrying no hypotheses at all.

Short of Lean-verified on the anchoring half. erdosproblems.com hosts this as a proof claim under its standing disclaimer that listing is "no guarantee of proof correctness" - it has not accepted the claim - and nobody without a stake has audited the informal-to-formal correspondence. The Lean was not built here - no toolchain. No referee has read it, and Green expects a human-written exposition to take months.

Sources

FrontierStep on Long prime gaps · ≫log⁡Xlog⁡2X/log⁡4X\gg \log X \log_2 X / \log_4 X · a step on the frontier, since improved

Changelog2 changes

Discussion