Erdős and Prachar's question: do the increases of $p_n/n$ have positive lower density?

Erdős problem #968 · erdosproblems.com/968

Let $p_n$ be the $n$ th prime and $u_n=p_n/n$ . Erdős and Prachar (1962) proved $\sum_{p_n<x}|u_{n+1}-u_n|\asymp(\log x)^2$ and that the set of $n$ with $u_n>u_{n+1}$ has positive density, and asked about the reverse inequality. Since $u_n<u_{n+1}$ is equivalent to $p_{n+1}-p_n>p_n/n\sim\log p_n$ , the question asks whether a positive proportion of prime gaps exceed the average gap, which needs control of how often gaps are large rather than of the largest gaps. Positive proportions were known only for gaps above a fixed fraction (about $0.579$ ) of $\log p_n$ . Does the set of $n$ with $p_n/n<p_{n+1}/(n+1)$ have positive lower density?

Result: Proved(see note)
Status: Candidate (review pending)
AI contribution: AI-discovered
Method: Argument
Field: Distribution of prime gaps
Posed by: Paul Erdős and Karl Prachar (Abh. Math. Sem. Univ. Hamburg 1962, p. 256); Erdős Problem #968
Year posed: 1962
Years open: 64y
Solved: 2026-09-25
Model: Unreleased internal OpenAI model
Vendor: OpenAI
Collaborators: —
Verification: Lean-checked, statement unaudited
Publication: Announced
Collection: OpenAI math release (October 2026), version adc7f12
Significance: 15 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Theorem 1.1: for every fixed $C>0$ there are $c(C)>0$ and $N_0(C)$ with $\#\{n\le N:p_{n+1}-p_n>C\log p_n\}\ge c(C)N$ for all $N\ge N_0$ , with ordinary lower density and equal weight on prime indices. Corollary 1.2 (take $C=2$ ) answers Erdős-Prachar: the increases of $p_n/n$ have positive lower density. The main theorem is stronger than the posed question. The constant $c(C)$ is not made explicit or compared with the Poisson prediction $e^{-C}$ , and the further questions recorded with Problem #968 on $u_n<u_{n+1}<u_{n+2}$ and $u_n>u_{n+1}>u_{n+2}$ are not addressed.

What the AI did

The release README says all results in the release were produced by an unreleased internal OpenAI model with one fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This family is not among the README's exceptions (the Hodge conjecture for CM abelian varieties, and the Re(s) > 11/12 zero-free region whose write-up was human-edited). The manuscripts are authored 'OpenAI' and name no human author. The release also formalizes both the main theorem and the corollary in Lean.

Verification

No independent mathematician has checked this yet. Checked here: Theorem 1.1, Corollary 1.2 and its short proof were read against Erdős Problem #968. Lean: lean/docs/026.md links ComparatorChallenges/PrimeGaps (theorem OAI.Problem344.large_gaps_and_ratio_density, solution module OAI.NumberTheory.PrimeGaps.RatioCorollary, file exists at the pinned commit), not in formalization.yaml. The statement was read: for every $C>0$ there are $c>0$ and $N_0$ with at least $cN$ indices $n\le N$ having $p_{n+1}-p_n>C\log p_n$ for all $N\ge N_0$ , and the set of $n$ with $p_n/n<p_{n+1}/(n+1)$ has positive lower asymptotic density. That is the headline. Not rebuilt here.

Sources

Lean proofLean proof (OAI.Problem344.large_gaps_and_ratio_density)
CodeOpenAI math release: Positive lower density of large prime gaps
Problem recordErdős Problem #968 (erdosproblems.com)

Erdős and Prachar's question: do the increases of pn/np_n/npn​/n have positive lower density?

What was actually shown

What the AI did

Verification

Sources

Discussion

Erdős and Prachar's question: do the increases of $p_n/n$ have positive lower density?