---

Claim. The manuscript Positive lower density of large prime gaps of the OpenAI mathematics release, dated 25 September 2026 and authored by OpenAI, has the intake card openai_2026_positive_lower_density_large_prime_gaps; the release's README says that its manuscripts were produced by an unreleased internal OpenAI model and that the collection includes results at different stages of verification. The manuscript states as its Theorem 1.1, and claims to prove, that for every fixed real $C>0$ there are constants $c(C)>0$ and $N_0(C)$ such that, for every $N\ge N_0(C)$,

$$\#\{1\le n\le N:\ p_{n+1}-p_n>C\log p_n\}\ \ge\ c(C)\,N,$$

where $p_n$ is the $n$th prime. Its Corollary 1.2: the set of $n\ge1$ with $p_n/n<p_{n+1}/(n+1)$ has positive lower asymptotic density. The manuscript's proof of the corollary (p. 2) is three lines: the inequality $u_n<u_{n+1}$ for $u_n=p_n/n$ is equivalent to $p_{n+1}-p_n>p_n/n$, the prime number theorem gives $p_n/n\sim\log p_n$, and Theorem 1.1 with $C=2$ applies after the finitely many $n$ with $p_n/n\ge2\log p_n$ are discarded. The manuscript cites the question to Erdős and Prachar's paper of 1961, p. 256 (library card erdos_1961_satze_und_probleme_uber_german), and says that the corollary answers it affirmatively. The argument offered for the theorem uses a weight, built as the square of a signed sum of smooth divisor sums, that detects a prime in an interval $(m,m+h]$ of length $h\asymp\log X$ while giving the adjacent interval $(m+h,m+2h]$ arbitrarily small weighted prime mass; a counting lemma (Lemma 2.2) turns such starts $m$ into distinct consecutive gaps longer than $h$, each prime being selected by at most $h$ starts. The inputs named are smooth divisor-sum correlations, the Bombieri--Vinogradov theorem and an average of the prime-tuple singular series; the construction is unconditional.

The question's density notion. The site's statement of Problem 968 asks for "positive density"; the problem page's precise Statement asks for positive lower density, which is what Erdős and Prachar ask on p. 256 of their paper (the card linked above), and which the formal-conjectures statement erdos_968 (FormalConjectures/ErdosProblems/968.lean at a pinned revision) also asks, with $u_n=p_n/(n+1)$ in its zero-based indexing of the primes. The corollary, as claimed, is exactly the precise Statement, so the claim is full. Whether the set has an asymptotic density at all is not addressed by the manuscript; that stronger reading is a variant recorded under the problem page's Formulation, and this claim does not settle it.

Formalization. The release's Lean tree at the pinned revision states the result as the challenge OAI.Problem344.large_gaps_and_ratio_density in ComparatorChallenges/PrimeGaps.lean (body sorry, the challenge form): the conjunction of Theorem 1.1, as the statement that for every $C>0$ some $c>0$ and $N_0$ make $cN$ a lower bound on the number of $n\in[1,N]$ with $C\log p_n<p_{n+1}-p_n$, with $p_n$ written Nat.nth Nat.Prime (n - 1), and of the positivity of the lower asymptotic density of $\{n\ge1: p_n/n<p_{n+1}/(n+1)\}$, where the lower density is defined as the supremum of the real $d$ such that the counting ratio is eventually at least $d$. The comparator configuration ComparatorChallenges/PrimeGaps.json names the solution module OAI.NumberTheory.PrimeGaps.RatioCorollary and permits the axioms propext, Quot.sound and Classical.choice; the folder OAI/NumberTheory/PrimeGaps/ exists at the pinned revision, and lean/docs/026.md says that the formalized supplement proves the corollary. The release's catalog lean/formalization.yaml has no entry for this manuscript. The build of the solution and the comparison of the challenge statement with the problem's statement are recorded under Acceptance.

Acceptance. Formalized. This corpus's verification built OAI.Problem344.large_gaps_and_ratio_density at the pinned revision with the toolchain leanprover/lean4:v4.34.1 and checked its axioms, which are exactly propext, Classical.choice and Quot.sound, with no sorry; the comparator challenge ComparatorChallenges/PrimeGaps.lean pins that declaration, and its fingerprint was found identical to the challenge. The release's declarations OAI.Problem344.positive_lower_density_prime_ratio_increases and OAI.LargePrimeGaps.main, which no challenge pins, were built and axiom-checked with the same three axioms. The statement agrees with the problem's: $p_n$ is Nat.nth Nat.Prime (n - 1), so $p_1=2$, and every use has $n\ge1$; the gap inequality $C\log p_n<p_{n+1}-p_n$ is compared in the reals with the natural logarithm, so no truncated subtraction occurs; the first conjunct quantifies as Theorem 1.1 does, for every $C>0$ some $c>0$ and $N_0$ for all $N\ge N_0$; the set is exactly $\{n\ge1: p_n/n<p_{n+1}/(n+1)\}$ with real division; and the lower density is the real supremum of a nonempty set of $d$ bounded by $1$, closed downward, so it is positive exactly when some $d>0$ is eventually at most the counting ratio, that is, when the liminf of the ratio is positive, and never through the junk value of an empty or unbounded supremum. The second conjunct is therefore the precise Statement, with "density" read as the lower density Erdős and Prachar asked for, and the claim is full; the theorem does not show that the set has an asymptotic density, the stronger reading kept open under the problem page's Formulation. Not reviewed: the manuscript is a release preprint with no journal record, no arXiv version and no outside review known here, and the release's README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification. The site's proof-claim tab for the problem was empty on 2026-10-07 and its label is OPEN (page last edited 31 March 2026).

Depends on. No page of this wiki.