Positive lower density of large prime gaps

1 paperLean

For every fixed C > 0, a positive proportion of consecutive prime gaps exceed \(C\log p_n\), throughout every sufficiently large initial segment of the primes. The proportion may depend on C. Consequently, the indices where \(p_n/n\) increases have positive lower density, answering Erdős and Prachar.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Positive lower density of large prime gaps

OpenAI · September 25, 2026

For every fixed C > 0, we prove that a positive proportion of consecutive prime gaps exceed \(C\log p\), where p is the smaller prime. The proportion is bounded below for every sufficiently large initial segment of the prime sequence, with a constant depending on C. It follows that the indices at which \(p_n/n\) increases have positive lower asymptotic density, answering a question of Erdős and Prachar.

Read PDF Download Source

Cite

@misc{OAI:Positive-lower-density-of-large-prime-gaps-September-25-2026,
  author = {{OpenAI}},
  title = {{Positive lower density of large prime gaps}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Positive-lower-density-of-large-prime-gaps-September-25-2026/main.pdf}{OAI:Positive-lower-density-of-large-prime-gaps-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Positive lower density of large prime gaps

Scope

The formalized supplement proves that the indices \(n\) for which \(p_n/n<p_{n+1}/(n+1)\) have positive lower asymptotic density, where \(p_n\) is the \(n\)th prime. Thus the normalized prime sequence has a positive-density set of increases. This is the prime-ratio corollary associated with the paper's theorem on a positive lower density of large prime gaps.

Comparator links

Result	Comparator statement
Positive lower density of prime-ratio increases	PrimeGaps.lean

Scope note on GitHub →