Positive lower density of large prime gaps

Positive lower density of large prime gaps is the subject of a manuscript dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). Writing p_n for the nth prime, it claims that for every fixed C > 0 a positive proportion of indices n have p_n+1 − p_n > C log p_n, and deduces an affirmative answer to a question of Erdős and Prachar on the ratios p_n/n. This page summarizes the published claim and lists publicly available follow-up work.

Background

• According to the manuscript's introduction, Westzynthius (1931) proved that d_n/log p_n is unbounded, where d_n = p_n+1 − p_n; Erdős and Rankin gave quantitative lower bounds for exceptionally large gaps, refined by Ford, Green, Konyagin and Tao, by Maynard, and in their joint work. These results concern the size of the largest gaps, not the proportion of gaps exceeding a fixed multiple of log p.
• The same introduction cites Bazzanella, Languasco and Zaccagnini (2010), whose Theorem 5 gives positive proportions of prime starts for each fixed threshold below 2/3.454 = 0.579…, and Tao's empty-interval argument (2019), and stresses the difference between counting prime-free intervals and counting gaps. Gallagher (1976) derived Poisson statistics for prime counts in short intervals from a uniform Hardy–Littlewood prime-tuple hypothesis.
• Erdős and Prachar asked whether the indices at which p_n/n increases have positive lower density. This is Erdős problem 968.

The original result

• Claim. For every fixed real C > 0 there are c(C) > 0 and N₀(C) such that #{1 ≤ n ≤ N : p_n+1 − p_n > C log p_n} ≥ c(C)N for every N ≥ N₀(C) (Theorem 1.1). Corollary 1.2: the set of n with p_n/n < p_n+1/(n + 1) has positive lower asymptotic density.
• Method, as described in the manuscript. An adjacent-interval construction: nonnegative weights, squares of signed sums of smooth divisor sums, make a prime in (m, m + h] likely while the expected number of primes in (m + h, m + 2h] is arbitrarily small, with h = ⌊λ log X⌋. The last prime of the first interval then begins a gap longer than h, and each such prime is counted at most h times. The analytic inputs are smooth divisor-sum correlations, the Bombieri–Vinogradov theorem and an average of the prime-tuple singular series. The manuscript names Goldston–Yıldırım's correlation method and Maynard's multidimensional sieve as antecedents.
• Source. Positive lower density of large prime gaps in the openai/math repository (commit 1581d4c).
• Formalization, as described by the repository.
  • The scope note lean/docs/026.md describes the formalized supplement as the prime-ratio corollary.
  • The Comparator challenge PrimeGaps.lean states the theorem large_gaps_and_ratio_density. Its first conjunct is the large-gap statement of Theorem 1.1 for every C > 0, and its second is the corollary.
  • The accompanying PrimeGaps.json names the solution module OAI.NumberTheory.PrimeGaps.RatioCorollary and permits only propext, Quot.sound and Classical.choice.
  • In the repository, the first conjunct is OAI.LargePrimeGaps.main. The file lean/OAI/NumberTheory/PrimeGaps/Main.lean derives it from Lean statements named siegelWalfisz and bombieriVinogradov proved in the same development.
• Catalogue status. Google DeepMind's Formal Conjectures project marks erdos_968 in FormalConjectures/ErdosProblems/968.lean as "research solved", with a formal_proof link to RatioCorollary.lean in the openai/math repository. The change was made in pull request #6898 (merged 11 October 2026).

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 16 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates the PrimeGaps challenge "full" and notes that it states the large-gap theorem and the ratio corollary, with lower density defined through a supremum; records a sandboxed Comparator pass.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list PrimeGaps, so the challenge was accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-11	Formal Conjectures pull request #6898	Catalogue (formal statement)	Marks Erdős problem 968 as "research solved" and links the Lean proof in the openai/math repository.	Merged.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.