Erdős Problem #968
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`u n` is the normalized `n`th prime, defined as `pₙ / (n+1)` where `pₙ` is the `n`th prime (with `0.nth Nat.Prime = 2`). This corresponds to the classical sequence `(p₁/1, p₂/2, p₃/3, ...)` while using `Nat.nth Prime`'s `0`-based indexing; in particular, the denominator is always positive.
Attempts
submit one →Read our full write-up →
In 1961–62 Erdős and Prachar proved that p_n/n decreases at a positive proportion of indices n and asked whether it also increases at a positive proportion. This is Erdős problem #968. Since p_n/n < p_{n+1}/(n+1) says exactly that the gap p_{n+1} − p_n exceeds p_n/n, which is about log p_n − 1, the question asks for a positive proportion of prime gaps of at least roughly average size. The best unconditional threshold we know of was a positive proportion of gaps above 0.579·log p (Bazzanella, Languasco and Zaccagnini, 2010). On the problem's thread Terence Tao derived the answer from the Riemann hypothesis plus a pair-correlation estimate, and called the question close to the limit of current technology. OpenAI's 6 October release claims much more: for every fixed C, a positive proportion of gaps exceed C·log p. The proof averages over starting points with a weight built from smooth divisor sums over the second of two adjacent intervals of length λ·log X. Alternating signs between neighbouring dimensions make the weighted number of primes in that interval as small as wanted, while the first interval keeps its share. A bounded-multiplicity count then turns empty intervals into distinct gaps. Our main reading seat, an AI (Claude Opus 5.5), read all five sections line by line and found no gap; three further hostile AI seats, two on the mathematics and one on the sources, found none either. OpenAI's Lean proof (56 modules, 22,533 lines) replays on our machine with the standard axioms and a matching statement. It proves the Siegel–Walfisz and Bombieri–Vinogradov theorems along the way; Mathlib has neither, and the paper assumes Bombieri–Vinogradov. A kernel-checked bridge of ours carries the result to a verbatim copy of Formal Conjectures' erdos_968, which uses a different indexing and a different definition of lower density. Our own sieve to 2.3·10¹⁰ finds p_n/n increasing at between 39.7% and 42.1% of indices at all ten checkpoints from 10⁶ to 10⁹; a second implementation matches it exactly at 10⁶, 10⁷, 10⁸ and 10⁹. Nothing in the theorem is ours.
CLOSED