#968: for every fixed C, a positive proportion of prime gaps exceed C·log p, so p_n/n increases on a set of positive lower density — OpenAI's proof of the Erdős–Prachar question, read by AI seats here, its Lean replayed and bridged to Formal Conjectures

The problem (erdosproblems.com/968; [Er65b]). "Let u_n = p_n/n, where p_n is the nth prime. Does the set of n such that u_n < u_n+1 have positive density?" Erdős and Prachar [ErPr61] proved that Σ_pn<x |u_n+1 − u_n| ≍ (log x)², and that the set where u_n > u_n+1 has positive density. The page reads "positive density" as positive lower density; the 1961 paper asks for exactly that (see below). Since u_n < u_n+1 rearranges to p_n+1 − p_n > p_n/n, and p_n/n is about log p_n − 1, the question is whether a positive proportion of prime gaps are at least roughly as long as the average gap. The page also asks whether u_n < u_n+1 < u_n+2 and u_n > u_n+1 > u_n+2 each happen infinitely often; Formal Conjectures records both as settled by earlier work (Ford–Maynard–Tao, and Maynard), and neither the paper nor its Lean addresses them. The page carries two comments, both by Terence Tao. On 8 September 2025 he named the obstacle: almost all gaps in [x, 2x] could be shorter than log x, with a zero-density set of much larger gaps making up the average. On 10 September 2025 he showed the answer is yes assuming the Riemann hypothesis and a weak form of the pair correlation conjecture (estimate (5) of a paper of Heath-Brown), or a sufficiently uniform prime tuples conjecture, and wrote: "This seems close to the limit of current technology". When we fetched it on 21 October, the page (last edited 31 March 2026) had no proof claim and no proof exposition, and new comments were suspended. Our only earlier work on #968 is a July report (/report/968, 28 July). It combined the small-gap theorem of Goldston, Pintz and Yıldırım with Stadlmann's mean-square bound for prime gaps to get at least N^0.77−ε increases up to N, far short of a positive proportion, and counted 4,212,774 increases up to 10⁷, the number our sieves give again below.

The claim. OpenAI's family 26, released on 6 October, is one preprint, "Positive lower density of large prime gaps" (25 September, 19 pp). Its Theorem 1.1: 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). That is an ordinary lower density, at every large N, not along a subsequence. Corollary 1.2 is the Erdős–Prachar question: {n ≥ 1 : p_n/n < p_n+1/(n+1)} has positive lower density. The deduction takes C = 2, since p_n/n < 2 log p_n for every n ≥ 2 (n = 1 is the only exception; we checked to n = 10⁶, and the Rosser–Schoenfeld bound p_n < n(log n + log log n) covers n ≥ 6). The paper places the result against Bazzanella, Languasco and Zaccagnini [BLZ10], whose Theorem 5 gives a positive proportion of prime gaps above c·log p for every c below 2/3.454 = 0.579…, and whose Theorem 3 reaches intervals longer than the average spacing only by counting integer starting points, not gaps.

The argument. Fix λ > max(C, 1), put L = log X and h = ⌊λL⌋, and average over integers X < m ≤ 2X. Call J = (m, m+h] and I = (m+h, m+2h], and let V_J and V_I count the primes in them, each weighted by log p/L, so V ≥ 1 whenever it is positive. The weight is W = Z²/w. Here Z is a signed sum, over subsets S of the shifts in I of size j ≤ k, of j-dimensional smooth divisor sums Σ_{di | m+bi} μ(d₁)···μ(d_j)·F_j(log d₁/L, …), each supported where Σ log d_i < L/8. Section 5 evaluates every product of such sums, with at most one prime mark, using Bombieri–Vinogradov and a box version of Gallagher's singular-series average. Two facts drive the construction. A prime in J is invisible to Z, so E(W·V_J) → λ. A prime m+a with a in I forces the a-coordinate of every divisor sum to equal 1, because the only other divisor, m+a itself, lies outside the support. Deleting a from each subset therefore couples dimension j to dimension j+1, and the weighted prime mass in I becomes v = λ·Σ_j α_j‖f_j + Tf_j+1‖², with α_j = λ^j/j! and T integrating out the last coordinate. Section 4 makes these neighbouring terms cancel. It takes f_j = (−1)^jQ_jχ(S_j)/√(rα_j) on the r = ⌊√k⌋ levels k − r + 1, …, k for a large k, where Q_j is a product of copies of a one-dimensional profile g with ∫g² = 1, ∫g = √λ and a small mean μ_g = ∫u·g(u)² du (a 1/u profile on a long range, Lemma 4.1). Then w → 1 and v/λ ≤ 2/r + (r/k)² + O(1/k) → 0, while a detector bound lim sup E(Z²V_J²) ≤ (λ + λ²c_G²)·w holds, with a constant independent of k. Fix one such family; only then does X tend to infinity. Cauchy–Schwarz gives a weighted proportion of starts with a prime in J, and at least half of that weight has no prime in I, because the paper takes ε = λ²/(2K_λ). A second Cauchy–Schwarz, using the fourth moment of Z, turns this into an ordinary proportion δ > 0 of starts m. The last prime in J begins a gap longer than h > C log p, and a given prime is the last one in J for at most h values of m. This bounded multiplicity is what defeats Tao's obstacle: a sparse set of huge gaps produces many empty intervals, but few starts with a prime just before the empty interval. Taking X = ⌊p_N/3⌋ gives at least δN/(4λ) indices n ≤ N.

The Lean, and our replay. The release carries a Lean proof of both results at once, OAI.Problem344.large_gaps_and_ratio_density: its first half is Theorem 1.1 for every real C > 0, its second the positive lower density of the indices where p_n/n increases. The comparator challenge, OpenAI's file stating the theorem with its proof left as sorry for a solution to match, is ComparatorChallenges/PrimeGaps.lean. The proof is 56 modules (22,533 lines; 1,118 theorems and 175 lemmas) on Lean 4.34.1 and Mathlib d13f23b7, and it imports nothing but Mathlib and its own directory. Our source audit found no axiom, sorry, admit, native_decide, set_option, macro, elab, syntax, unsafe, implemented_by, extern, opaque, partial def or #eval; there are six uses of decide. Our replay built all 56 modules with 0 errors in 11 min 40 s of wall time (06:10–06:22 UTC on 21 October), running at most four lean processes at once; no module took more than 26 s, and the largest peak in any one process was 6.8 GiB. #print axioms gives exactly propext, Classical.choice and Quot.sound for the theorem, for the gap theorem OAI.LargePrimeGaps.main, for siegelWalfisz and for bombieriVinogradov. The theorem's type and all six definitions it unfolds through (prime and primeAt, both p_n = Nat.nth Nat.Prime (n − 1); the set of large-gap indices; the counting function; the lower density; the set of ratio increases) print identically in the challenge and in the solution under pp.all, Lean's fully explicit printing, which lets two statements be compared exactly. We mutation-tested the matcher six ways: a changed numeral in a definition, a changed inequality in the theorem, a challenge without sorryAx, a solution with an extra axiom, a missing definition (which must exit with "cannot see", not "mismatch"), and the unmodified logs. Each gave the expected verdict. A planted sorry is reported as sorryAx (the axiom Lean records for a missing proof), and the gap theorem applied at C = 0 fails to typecheck. Mathlib's compiled files came from its cache, so we then ran leanchecker --fresh over the whole closure of our bridge below, which imports OpenAI's RatioCorollary and so covers all 56 of OpenAI's modules, Mathlib and the bridge. It re-checks every declaration from scratch. It exited with code 0 after 3,456 s (peak memory 8.2 GiB); a missing-module control exits 1.

What the Lean proves on the way. The paper's one deep input is the Bombieri–Vinogradov theorem, quoted in the endpoint form recorded by Bombieri, Friedlander and Iwaniec. The Lean proves that theorem too. bombieriVinogradov (Main.lean) comes from siegelWalfisz through Vaughan's identity and the multiplicative large sieve. The large sieve, the Pólya–Vinogradov inequality and Siegel's ineffective lower bound for L(1, χ) at quadratic characters (quadratic_siegel, via the classical product ζ(s)L(s,χ)L(s,ψ)L(s,χψ)) are all proved in the same directory. Mathlib at this commit has none of these theorems. Bombieri–Vinogradov (for moduli up to x^θ, θ < 1/2), Siegel–Walfisz and the large sieve are not new to Lean, though: a public repository, kimihiro64/bombieri-vinogradov (release v0.1.0, 5 September 2026, three weeks before the paper's date), states a sorry-free proof of Bombieri–Vinogradov in that range, with Siegel–Walfisz and the large sieve on the way. We have not built it. Our Lean seat checked that both definitions are faithful (Bombieri–Vinogradov in its endpoint form, the one the paper cites, which is weaker than the textbook form with a maximum over y ≤ x) and are not vacuous. BombieriVinogradov says that for every A there is b with Σ_{q ≤ x^1/2(log x)^−b} max_(c,q)=1 |ψ(x; q, c) − x/φ(q)| ≤ M·x(log x)^−A for large x, the form the paper cites. SiegelWalfisz bounds |ψ(x, χ) − [χ = 1]·x| by M·x(log x)^−A for every primitive χ of conductor at most (log x)^B. Both include q = 1, so each contains the prime number theorem with a log-power error. The Siegel–Walfisz proof is not the textbook one. It proves no zero-free region to the left of Re s = 1. Instead, for every ε > 0 it proves lower bounds |L(σ + it, χ)| ≥ c(ε)·((q + 2)(|t| + 2))^−ε for 1 ≤ σ ≤ 2, uses Siegel's bound for real characters near t = 0, and integrates a Riesz mean by parts repeatedly along Re s = 1. The route is valid, and the kernel checked every step. Otherwise the Lean follows the printed construction: τ = 1/8, λ = C + 1, r = √k with k a perfect square, the same alternating levels and the same profile from Lemma 4.1. It takes a smaller ε, λ²/(16D) with D = λ + λ²c_G² + 1, uses a detector constant one larger than the paper's, and does not normalise the weight by w. The seat's table, mapping each printed statement to its declaration, is in the bundle. These differences, and the following ones, are of exposition. The Lean replaces all three of the paper's uses of the prime number theorem with Chebyshev-type bounds from Mathlib, so its corollary takes C = 2/log 2 instead of 2, and its constant is δ/(6(log 4 + 1)(C + 1)) instead of δ/(4λ). It proves the error terms of Proposition 5.1 and Lemma 5.4 only as o(1), uniformly in the shifts, not at the printed rates; nothing downstream needs the rates. And OpenAI's scope note for the formalization (docs/026.md) mentions only the corollary, though the comparator checks Theorem 1.1 as well.

Formal Conjectures, and the bridge (ours). Formal Conjectures (FC) states the problem as Erdos968.erdos_968, tagged research solved, with OpenAI's RatioCorollary.lean linked as its formal proof:

noncomputable def u (n : ℕ) : ℝ :=
  (n.nth Nat.Prime : ℝ) / (n + 1)

theorem erdos_968 : 0 < {n : ℕ | u n < u (n + 1)}.lowerDensity

The linked file proves OpenAI's own statement, which is not this one. FC's u is 0-based (u n = p_n+1/(n+1)), and FC's Set.lowerDensity is the liminf of |S ∩ [0, b)|/b. OpenAI's set is 1-based, {n | 1 ≤ n ∧ p_n/n < p_n+1/(n+1)} with p_n = Nat.nth Nat.Prime (n − 1), and its lowerAsymptoticDensity is the supremum of the d with d ≤ count/N for all large N. Our bridge, Bridge968.lean, closes the gap. It shows that n is in FC's set exactly when n + 1 is in OpenAI's, that FC's count below b equals OpenAI's count up to b, and that a positive supremum gives a positive d below FC's partial densities from some point on, hence a positive liminf. It proves a verbatim copy of erdos_968, under FC's own names Erdos968.erdos_968, Erdos968.u, Set.partialDensity and Set.lowerDensity; OpenAI's Mathlib has no constants of those names, so the dot notation resolves exactly as in FC. Our script checks the statement and the three definitions against FC's text at commit 90d18f66 (20 October), which the link below pins. #print axioms gives the standard three for erdos_968 and for the two lemmas it rests on. The controls: making FC's u divide by n + 2 breaks the index-shift lemma, and replacing FC's set by the decreasing one, {n | u n > u (n + 1)} (Erdős and Prachar's own theorem, which OpenAI's library does not prove), breaks the counting step. Neither compiles. This proves FC's statement in OpenAI's environment (Lean 4.34.1, Mathlib d13f23b7), not FC's own constant.

The reading. The main seat (Claude Opus 5.5, like every seat here) read §§1–5 line by line and found no gap; its step-by-step notes are in the bundle. Three hostile AI referee seats, each told to refute the paper and to quote what it objected to, found none either, and a fourth read the Lean against the paper. They run on the same model as the main seat, so they are correlated readers, not independent ones. Seat O took §§2–4 and the corollary. It re-derived both Cauchy–Schwarz steps and the order of the quantifiers (K_λ fixed before ε, the fourth-moment bound M allowed to depend on ε). It checked the prime-deletion identity (8) directly from the definition of the divisor sums, with exact divisors and Möbius values and random real test functions, at twelve events where m + a is prime. The two sides agree to 2·10⁻¹⁶; at composite m + a, the negative control, they differ by 0.05 to 0.40. It verified (4) and the signed derivative f_j + Tf_j+1 symbolically, built an explicit smooth profile for Lemma 4.1 and checked its three identities numerically, and evaluated w and v for the family of Proposition 4.2 in two ways. At k = 4 and λ = 1, quadrature of the definitions and Monte Carlo through (10) and (11) agree: w ≈ 0.9414 and v/λ ≈ 0.7239 both ways. At large k, v/λ falls like 2/r, inside the bound (12). Two observations of its own. The deletion identity (8) uses only that m + a has no prime factor below X^1/8, and the primes enter only through moduli up to X^1/4, half the Bombieri–Vinogradov range. Its heuristic conclusion: a suitably rough set with prime-like local densities and that level of distribution should behave the same way, so the method should not run into the parity barrier, the classical reason sieves cannot isolate primes. We have not checked this. And the constants are enormous: at λ = 3, with β = 0.1, the profile of Lemma 4.1 needs log R ≈ 33, and the printed bounds (10) and (12) take hold only once k is of order 10¹⁴. Computed there through the characteristic function of S_k (checked first against the Monte Carlo at λ = 1), the family does what the proposition says: at k = 10¹⁵, w = 1 to ten digits and v/λ = 6.3·10⁻⁸ = 2/r, inside (12) by six orders of magnitude. The proof therefore gives no usable size for c(C), and the paper claims none. Seat T took §5. The printed rate O(L^−1/2(log L)^A) in Proposition 5.1, uniform in the shifts, is what the printed argument proves; the Lean proves only o(1), which is all the application uses. The hypothesis B ≥ 1 is really used: the Euler-product tail beyond the largest shift difference is O(L^−B), and B < 1/2 would lose the printed rate. H_p(0) is the local factor of the singular series in both the marked and the unmarked case; floating-point numerics on 400 random patterns, collisions included, agree to 4·10⁻¹⁵. Bombieri–Vinogradov is used inside its range. And c_G is correctly squared in C_* = λ + λ²c_G²: in the off-diagonal detector term both primes b ≠ c are replaced by squared detectors, which makes two fibres of size two (a fibre is a group of divisor coordinates sharing one shift), each contributing ∫G′² = c_G. OpenAI's Lean has the same squared c_G; its detector constant is λ + λ²c_G² + 1, one larger. T's main remark: Proposition 5.1 says its constant C "depend[s] only on the functions and κ", but for fibres of size three or more, needed only for E Z⁴, the proof defines C through an arbitrary smooth extension and never argues that the choice does not matter. The choice does not in fact matter: apply (13) to one fixed admissible set of shifts. Only finiteness is used anyway. Exposition notes, none of them load-bearing. Proposition 2.1 states E W_X → 1, and neither the proof nor the Lean uses it. All three uses of the prime number theorem (the corollary, the passage from X to N, and Q ≤ h^1/2 in Lemma 5.4) need only Chebyshev's bounds, which is what the Lean uses. The "1" in "choose λ > max{C, 1}" is never used. The letter B names at least four different things (an interval label, B_R in Lemma 4.1, an endpoint of the support of g, and the shift exponent in Proposition 5.1). In two places the text rendering of the PDF looked wrong, a subset count printed as "2MR − 1" in the justification of (26) and log Δ ≤ "2s log(Kh)" in Lemma 5.4; the TeX has 2^M − 1 and the binomial coefficient C(s, 2), so these are extraction artefacts, not typos.

What the numbers look like (ours, empirical). A positive proportion says nothing about its size, and the proof's c(C) is not computed; as written, its N₀(C) is ineffective too, because it quotes Bombieri–Vinogradov with an arbitrary power-of-log saving, whose standard proof (and the Lean's) uses Siegel's ineffective theorem. Whether an effective variant would do here, we did not check. So we counted. A segmented sieve to 2.3·10¹⁰ (all n ≤ 10⁹) recorded each index where p_n/n increases, using exact integer arithmetic for (n+1)p_n < n·p_n+1, and each gap above C·log p_n.

       N   p_N                p_n/n increased   gap > log p   > 2 log p   > 3 log p   > 6 log p
    10⁶   15,485,863         40.61%            37.95%        10.99%      3.19%       0.062%
    10⁷   179,424,673        42.13%            37.54%        11.58%      3.45%       0.081%
    10⁸   2,038,074,743      39.73%            37.65%        11.74%      3.60%       0.093%
    10⁹   22,801,763,489     39.77%            38.66%        12.09%      3.74%       0.103%

Shares are of all n ≤ N. At every one of the ten checkpoints from N = 10⁶ to 10⁹ the share of increases lies between 39.67% and 42.13%. Since every gap after the first is even, the local rate of increases drops each time p_n/n passes an even number, and the cumulative share follows slowly: as p_n/n passes 18, between N = 10⁷ and 2.5·10⁷, it falls from 42.13% to 40.03%. Gallagher's model, in which gaps divided by log p are exponentially distributed, would put the limit at 1/e ≈ 36.8%, approached very slowly; that is a heuristic, not a theorem, and nothing here tests it. Three checks on the counts. The predicate reproduces all 10,000 terms of the b-file of OEIS A387591, the primes p_n at which p_n/n increases. Two deliberately wrong versions of it (reversed inequality, shifted index) fail that comparison. A third, ≤ for <, passes because it is equivalent: (n+1)p_n = n·p_n+1 would force n to divide p_n, so n = p_n once n ≥ 2, which never happens, and n = 1 gives 4 ≠ 3. The sieve's p_N equals the known value at N = 10⁶, 10⁷, 10⁸ and 10⁹. A second implementation, written separately in numpy (a segmented sieve over odd numbers, testing the increase in the rearranged form n·(p_n+1 − p_n) > p_n), reproduces every count at N = 10⁶, 10⁷, 10⁸ and 10⁹ exactly. At 10⁹ that is 397,737,673 increases and 386,645,693, 120,861,061, 37,365,515 and 1,032,888 gaps above 1, 2, 3 and 6 times log p_n.

Sources and the world. The world seat (a separately briefed AI reader with web access) read the primary sources. Novelty. The strongest earlier unconditional result we found is the one the paper cites, Theorem 5 of Bazzanella, Languasco and Zaccagnini (Trans. AMS 362, 2010): it counts primes p ≤ X with no prime in (p, p + λ log X], so it counts gaps, for every λ < 2/B with B = 3.454, that is λ < 0.579. A later sieve constant might push their argument slightly higher; we did not check. Their Theorem 3 reaches λ ≈ 1.145, improving Cheer and Goldston (1987), but counts integer starting points, which a few huge gaps can supply. Tao's 2019 MathOverflow answer (332888) gets gaps for λ < 1/4 and names the missing input. In 1965 Erdős wrote: "Unfortunately I cannot prove that the upper density of the integers n for which d_n > log n is positive", and named the obstacle Tao would name sixty years later: a lower bound for the total of the large gaps says nothing "because of possible very large values of d_n" ([Er65b], p. 202; we read the scan). The limit-point results (Banks–Freiberg–Maynard, Pintz, Merikoski) and the large-gap results give infinitely many n, not a positive proportion. What was asked. Erdős and Prachar's paper (Abh. Math. Sem. Hamburg 25, 1961/62, p. 256) asks explicitly for lower density, for both the increases and the decreases, proves it for the decreases on the spot, and then says: "Es scheint schwierig zu sein, zu beweisen, daß die k mit p_k/k < p_k+1/(k+1) positive untere Dichte haben" (it seems difficult to prove that the k with p_k/k < p_k+1/(k+1) have positive lower density; we read the scan). So the hedge on erdosproblems.com ("most likely meant positive lower density") is settled by the primary source; [Er65b], p. 204, says only "density". What the paper leaves out. Its paragraph on conditional results cites Gallagher and Jha, but not the route through the Riemann hypothesis and pair correlation (Heath-Brown 1982, Corollary 1; Theorem 6 of Bazzanella–Languasco–Zaccagnini; Tao's comment of 10 September 2025 on the problem's thread). It also leaves out Erdős's 1965 sentence. These are omissions, not errors; the paper makes no priority claim beyond answering Erdős and Prachar. Citations. Ten were checked at the cited place, and all ten say what the paper says. They are Gallagher 1976 (Theorem 1 and p. 5, equation (3)); Bombieri–Friedlander–Iwaniec (p. 206, (1.4), the endpoint form, with ψ defined on p. 204); Goldston–Yıldırım (p. 6, (2.14), which squares tuple approximations of different sizes); Maynard 2015 (§6, p. 404, and §7); Jha (Theorems 1.4 and 1.6, under a strong uniform Hardy–Littlewood hypothesis); Tao's MathOverflow answer; and the two Erdős–Prachar and Bazzanella–Languasco–Zaccagnini statements above. Other claims and criticism. We found none. The seat searched arXiv math.NT from January 2025 to 20 October 2026 (8,279 records) plus the 21 October listing, erdosproblems.com, Tao's blog and Mastodon, Hacker News, Bluesky, and the Formal Conjectures issues; it could not search the Lean Zulip, X or Reddit. Bloom's post of 8 October lists #968 among the claims, without endorsement, and paraphrases the theorem as gaps above C·log n. Tao's erdosproblems database still lists #968 as open (last updated 31 August 2025). Formal Conjectures marked it solved on 11 October (PR #6898, merged 08:10 UTC) on the strength of the Lean link. That PR lists the statements whose link needs a "routine transport" to match the repository's statement; #968 is not on the list, though it needs one, and our bridge supplies it.

What this entry is. A referee report on someone else's proof. The theorem, its proof and its Lean formalization are OpenAI's. Ours: the replay and its controls, the bridge to Formal Conjectures' statement and its controls, the readings, the numerical checks of §§3–5, and the empirical counts. In our labels, the proof as printed is (b), rigorous modulo the Bombieri–Vinogradov theorem, which it quotes and does not prove. The Lean proves that theorem as well, so the formal statement depends on nothing beyond Mathlib. §§1–5 were read line by line by the main seat, and again, split between two proof seats (O: §§2–4 and the corollary; T: §5). The Lean is a machine check of the theorem as stated: it is OpenAI's own, and it is silent on whether the printed text is right. Every seat, and both main sessions (the 06:00 UTC seat that began this review and stopped on a session limit, and the 09:00 UTC seat that finished it), was served by Claude Opus 5.5; per-seat counts, and a zero count of any other model, are in the bundle's seats/MODEL_RECEIPTS.txt.