---

Claim. The manuscript A quadratic bound for Jacobsthal's function of the OpenAI mathematics release, dated 25 September 2026 and authored by OpenAI (its intake card is openai_2026_quadratic_bound_jacobsthal_function), proves as its Theorem 1.1 that Jacobsthal's function $h(k)$, the least $m$ such that every $m$ consecutive integers contain one coprime to any given positive integer with at most $k$ distinct prime factors, satisfies

$$h(k)\ll\frac{k^2}{(\log\log 3k)^2},$$

uniformly in the modulus and in the position of the interval. The release states that its manuscripts were produced by an internal OpenAI model and come at different stages of verification, not all with Lean formalizations. Its abstract presents this as a yes to Jacobsthal's quadratic-bound question, the displayed question of Problem 970. The manuscript states the covering form of this problem. Its introduction observes that $h(k)-1$ is the greatest length of an interval that the divisibility classes of at most $k$ primes can cover, and calls one prescribed residue class at each prime below a cutoff another form of the same covering problem, through the Chinese remainder theorem. Its Theorem 1.2 (the library's Theorem 1.2 page) is that covering statement at one interval length: for every large $z$ and every choice of one class $a_p\pmod p$ for each prime $p\le z$, at least $cYV_0/B^2>0$ integers of $[1,Y]$, $Y=\lfloor z^2/(\log z)^2\rfloor$, avoid every class. So no choice of classes covers $[1,Y]$, and

$$Y(z)<\Bigl\lfloor\frac{z^2}{(\log z)^2}\Bigr\rfloor$$

for every large $z$: a saving of $(\log x)^2$ over Iwaniec's $Y(x)\ll x^2$ and a yes to the first displayed question, $Y(x)=o(x^2)$, directly from the manuscript. The manuscript does not name $Y(x)$ or Problem 687, and its catalog entry speaks only of Jacobsthal's question and the displayed bound of Problem 970: the reading of Theorem 1.2 as a bound on $Y(z)$ is made here and in the Status paragraph of the problem page.

Covers. The first displayed question, $Y(x)=o(x^2)$, with the saving $(\log x)^2$ over Iwaniec's $Y(x)\ll x^2$ from Theorem 1.2. Not covered: the second displayed question, $Y(x)\ll x^{1+o(1)}$, and the estimate of $Y(x)$, which if the claim stands lies between the lower bounds on the problem page and $x^2/(\log x)^2$.

Formalization. The release's Lean tree at the pinned revision states the theorem as the challenge erdos_970_iterated_log, of type NumberTheoryLean.Targets.JacobsthalIteratedLog, in ComparatorChallenges/JacobsthalImproved.lean (body sorry, the challenge form) and proves a declaration of the same name and type in OAI/NumberTheory/Jacobsthal/Conclusions/IteratedLogBound.lean. The target asserts a constant $C>0$ such that every $k\ge1$ has some $m\le Ck^2/(\log\log 3k)^2$ with IsJacobsthalBound k m, and that predicate says that for every positive $n$ with at most $k$ distinct prime factors and every integer $a$, some $a+i$ with $0\le i<m$ is coprime to $n$. The release's catalog lean/formalization.yaml lists the manuscript and records the plain quadratic declaration erdos_970_quadratic (Conclusions/QuadraticBound.lean, comparator configuration ComparatorChallenges/Jacobsthal.json) as its formalized main result. The tree also holds the covering statement for one class per prime, as interior declarations: cutoffSurvivors Y z residue (OAI/NumberTheory/Jacobsthal/Primes/LargePrimeDeletion.lean) is the set of $i<Y$ with $i\not\equiv$ residue p $\pmod p$ for every prime $p\le z$, and OAI.Erdos970.Erdos970Final.source_root_survivor_lower (Conclusions/SourceRootCompletion.lean, with sourceY z the floor of $z^2/(\log z)^2$) bounds the survivor count below, for every residue choice and all large $z$, in the form Theorem 1.2 takes in the tree; RootCutoffSurvivors.cutoff_lower_of_root_lower carries that bound to cutoffSurvivors, and erdos_970_quadratic is proved from it. None of these is on the comparator surface or was audited for fidelity, and nothing in the tree names $Y(x)$, the primorial $P(x)$ or this problem, so the formalization reaches this problem only through the unformalized readings above. The corpus's verification built erdos_970_quadratic at the pinned revision, found its axioms to be propext, Classical.choice and Quot.sound only, and audited its statement against the formulation of Problem 970, as that problem's claim page records; that declaration concerns $h$, not $Y$, so formalized is not listed here. The survivor declarations are recorded from the source text and were not built or audited.

Acceptance. None. The manuscript is a release preprint with no journal record and no independent review known here, and the Lean statement the corpus built and audited concerns $h$ rather than this problem's covering function, so no evidence is listed. The claim enters as claimed and the problem's standing stays open.

Depends on. Theorem 1.2 of the manuscript, whose direct reading as a bound on $Y(z)$ is a remark made here, not a reviewed result.