View source for 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 ([https://github.com/openai/math github.com/openai/math]). Writing ''p''<sub>''n''</sub> for the ''n''th prime, it claims that for every fixed ''C'' &gt; 0 a positive proportion of indices ''n'' have ''p''<sub>''n''+1</sub> − ''p''<sub>''n''</sub> &gt; ''C'' log ''p''<sub>''n''</sub>, and deduces an affirmative answer to a question of Erdős and Prachar on the ratios ''p''<sub>''n''</sub>/''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''<sub>''n''</sub>/log ''p''<sub>''n''</sub> is unbounded, where ''d''<sub>''n''</sub> = ''p''<sub>''n''+1</sub> − ''p''<sub>''n''</sub>; 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''<sub>''n''</sub>/''n'' increases have positive lower density. This is Erdős problem 968.

== The original result ==
* '''Claim.''' For every fixed real ''C'' &gt; 0 there are ''c''(''C'') &gt; 0 and ''N''<sub>0</sub>(''C'') such that #{1 ≤ ''n'' ≤ ''N'' : ''p''<sub>''n''+1</sub> − ''p''<sub>''n''</sub> &gt; ''C'' log ''p''<sub>''n''</sub>} ≥ ''c''(''C'')''N'' for every ''N'' ≥ ''N''<sub>0</sub>(''C'') (Theorem 1.1). Corollary 1.2: the set of ''n'' with ''p''<sub>''n''</sub>/''n'' &lt; ''p''<sub>''n''+1</sub>/(''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'' + 2''h''] 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.''' [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Positive-lower-density-of-large-prime-gaps-September-25-2026 ''Positive lower density of large prime gaps''] in the openai/math repository (commit <code>1581d4c</code>).
* '''Formalization, as described by the repository.'''
** The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/026.md lean/docs/026.md] describes the formalized supplement as the prime-ratio corollary.
** The Comparator challenge [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/PrimeGaps.lean PrimeGaps.lean] states the theorem <code>large_gaps_and_ratio_density</code>. Its first conjunct is the large-gap statement of Theorem 1.1 for every ''C'' &gt; 0, and its second is the corollary.
** The accompanying <code>PrimeGaps.json</code> names the solution module <code>OAI.NumberTheory.PrimeGaps.RatioCorollary</code> and permits only <code>propext</code>, <code>Quot.sound</code> and <code>Classical.choice</code>.
** In the repository, the first conjunct is <code>OAI.LargePrimeGaps.main</code>. The file [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/OAI/NumberTheory/PrimeGaps/Main.lean lean/OAI/NumberTheory/PrimeGaps/Main.lean] derives it from Lean statements named <code>siegelWalfisz</code> and <code>bombieriVinogradov</code> proved in the same development.
* '''Catalogue status.''' Google DeepMind's Formal Conjectures project marks <code>erdos_968</code> in [https://github.com/google-deepmind/formal-conjectures/blob/7db2ea3b91bfbd0ab620215163e6c488bbb916d5/FormalConjectures/ErdosProblems/968.lean FormalConjectures/ErdosProblems/968.lean] as "research solved", with a <code>formal_proof</code> link to <code>RatioCorollary.lean</code> in the openai/math repository. The change was made in [https://github.com/google-deepmind/formal-conjectures/pull/6898 pull request #6898] (merged 11 October 2026).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 16 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates the <code>PrimeGaps</code> 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) does not list <code>PrimeGaps</code>, so the challenge was accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-11 || [https://github.com/google-deepmind/formal-conjectures/pull/6898 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.

[[Category:OpenAI results]]