A tilted residue-class construction for long prime-free intervals
partialconfidence 70%
VibeMathed reports this item as partial. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
How large can the gap between consecutive primes be, infinitely often? Writing $\log_k$ for the $k$-fold iterated logarithm, Erdős asked (problem #4, a \$10,000 prize) whether $p_{n+1}-p_n \gg C\log n\log_2 n\log_4 n/(\log_3 n)^2$ for every $C$; that was settled in 2016, and the record bound since has been Ford-Green-Konyagin-Maynard-Tao's $p_{n+1}-p_n \gg \log n\log_2 n\log_4 n/\log_3 n$. This work claims a stronger bound, $G(T)\gg \log T\log_2 T/\log_4 T$, an improvement by a factor of $\log_3 T/(\log_4 T)^2$, together with $Y(X)\gg X\log X/\log_3 X$ for the covering problem behind it.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
GPT 5.6 Sol
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.
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 $\texttt{sorry}$, no $\texttt{admit}$, no $\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.
A Tilted Residue-Class Construction for Long Prime-Free Intervals
Claims $G(T)\gg\log T\log_2 T/\log_4 T$ against FGKMT's $\log T\log_2 T\log_4 T/\log_3 T$, a gain of $\log_3 T/(\log_4 T)^2$, together with $Y(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_3 N$ over that procedure. The [FGKMT] paper also wins a $\log_3 N$. These wins are essentially independent of one another so one now wins basically $(\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".
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.