What was already known
Ford–Green–Konyagin–Maynard–Tao’s 2018 bound was G(T)≫log T log₂ T log₄ T/log₃ T. The paper reuses their Maynard weight and hypergraph-covering theorem but changes the intermediate sieve. OpenAI’s later GPT 6 Astra bound is stronger and is assessed separately.
AI involvement
The manuscript credits GPT 5.6 Sol with the new tilt. DottedCalculator prompted and submitted it; Boris Alexeev later formalized the stated bounds, while Ben Green and Thomas Bloom explained the sieve.
The model is credited as author of the new tilt, while the named humans submitted, reviewed and formalized the result.
Importance
Improves the Ford–Green–Konyagin–Maynard–Tao lower-bound line through a new intermediate sieve.
Limitations
The construction reuses the earlier Maynard weight and hypergraph-covering theorem. A later GPT 6 Astra result gives a stronger asymptotic bound. The model is named GPT 5.6 Sol in the manuscript and GPT 5.6 Pro in the filing.
Technical verification
Alexeev’s Lean module states both all-sufficiently-large covering and prime-gap bounds with no theorem hypotheses; this is a source-reported machine check. Expert discussion is supportive but does not document a complete separate human proof check.
Formal checking
Lean proofs covering_theorem and prime_gap_corollary, importing the tilted construction development
- Checker
- Boris Alexeev’s Erdos4Tilted Lean development
- Scope
- Covering theorem and prime-gap corollary at every sufficiently large real endpoint
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Green and Bloom identify the novel probabilistic intermediate sieve and its relation to the imported 2018 covering machinery.
Correction and publication history
Improves the Ford–Green–Konyagin–Maynard–Tao lower-bound line through a new intermediate sieve.
Read this published revision