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

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.

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: Boris Alexeev (Lean formalisation)
Verification: Lean-checked, statement unaudited
Publication: Announced
Significance: 50 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

The claimed bound is $G(T)\gg\log T\log_2 T/\log_4 T$ , against the previous record $\log T\log_2 T\log_4 T/\log_3 T$ of Ford-Green-Konyagin-Maynard-Tao - an improvement by $\log_3 T/(\log_4 T)^2$ . The construction biases a random residue-class sieve toward the zero residue with a Rankin-type tilt, which gives an exact survival law and permits an all-fiber block construction for composites, while a Maynard weight and FGKMT's quantitative hypergraph covering theorem handle the surviving primes.

What it does not do. Erdős problem #4 as posed was settled in 2016 by Maynard and by Ford, Green, Konyagin and Tao; this improves the record, it does not answer the question. It also falls short of the lower bound $>(\log n)^{1+c}$ that Erdős reserved the $10,000 for, since $\log\cdot\log_2/\log_4$ is still $(\log n)^{1+o(1)}$ . The likely truth is believed to be around $(\log n)^2$ .

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, so the model is credited as the author of the mathematics rather than as an assistant to one. There is no acknowledgements section and no human contributor named anywhere in the manuscript.

That makes this the least ambiguous AI-discovered entry in the catalog: elsewhere a human at least writes up, directs or checks the argument and says so. Here the only named human contribution is downstream and formal - Boris Alexeev's Lean development, which transcribes the manuscript's two main statements rather than producing them.

What the paper does claim about its own inputs: "The only external inputs are classical prime-distribution theorems and two precisely stated results of Ford-Green-Konyagin-Maynard-Tao; every hypothesis of those results is verified explicitly."

Verification

Lean-checked. The formalisation was audited at source here on 30 August 2026, and it is unusually clean, but it was not built.

Across the 403 Lean files of the Erdős 4 development (56,614 lines) there is no $\texttt{sorry}$ , no $\texttt{admit}$ , no $\texttt{native\_decide}$ - the one grep hit is the English word "admit" in a docstring - and, notably, not a single declared $\texttt{axiom}$ . The Ford-Green-Konyagin-Maynard-Tao inputs the paper names are therefore neither axiomatised nor carried as hypotheses: the module header states that "the final theorems have no analytic or covering hypotheses", and the repository's own notes say the development "also proves the stronger FGKMT18 bound".

Statement fidelity was checked on the terminal theorem, which is written in primitive Mathlib terms rather than through a bespoke abstraction - $\texttt{Nat.nth Nat.Prime}$ for the primes, no hypotheses - and says exactly $G(T)\gg\log T\log_2 T/\log_4 T$ .

Not Lean-verified, because the kernel half is unconfirmed: there is no Lean toolchain on this machine, and the repository's README says only that its projects build "last I checked" and that a build "might take many hours". Nobody independent has audited the informal-to-formal correspondence either. The manuscript is unrefereed and hosted in a GitHub repository rather than a preprint server - expected, since arXiv will not list a model as an author.

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

What was actually shown

What the AI did

Verification

Sources

Discussion