---

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, with the statement on its Theorem 1.1 page), states as its main theorem, and claims to prove, that Jacobsthal's function $h(k)$, the least $m$ such that every block of $m$ consecutive integers contains an integer coprime to any given positive $n$ with at most $k$ distinct prime factors, satisfies

$$h(k)\le C\,\frac{k^2}{(\log\log 3k)^2}\qquad\text{for every }k\ge1,$$

with one absolute constant $C>0$, uniformly over the set of prime divisors and the position of the block. This contains Jacobsthal's conjecture $h(k)\ll k^2$, the displayed question of Problem 970, with an iterated-logarithm saving. Of it, the quadratic bound $h(k)\le Ck^2$ is accepted here through the Lean declaration erdos_970_quadratic named below; the saving by $(\log\log 3k)^2$ is the manuscript's claim. The argument sieves one forbidden class at each prime up to $z$ with a lower-bound sieve at the critical parameter $2$ (Theorem 1.2 of the manuscript, a survivor count on an interval of length $z^2/(\log z)^2$), then removes the remaining large divisor primes by an upper sieve; the constant is not made explicit and, by the manuscript's stated conventions, need not be effective. The release's formalization page for its family 021 says that the order of magnitude of $h(k)$ is not determined.

Covers. The displayed question "is it true that $h(k)\ll k^2$?" is answered yes. One absolute $C>0$ gives $h(k)\le Ck^2$ for every $k\ge1$. Here $h$ counts $n$ by distinct prime factors, and a block of consecutive integers may start at any integer. The order-of-magnitude question, which carries the OPEN label, is not settled.

Formalization. The release's Lean tree at the pinned revision proves the declaration OAI.Erdos970.Erdos970Final.erdos_970_quadratic, in OAI/NumberTheory/Jacobsthal/Conclusions/QuadraticBound.lean, the main result the release's catalog lean/formalization.yaml lists for this manuscript. Its statement, JacobsthalQuadratic, fixes one real $C>0$ before $k$ and asks, for every $k\ge1$, for some $m\le Ck^2$ with IsJacobsthalBound k m; that predicate says that for every $n>0$ with at most $k$ distinct prime factors and every integer $a$, some $a+i$ with $0\le i<m$ has $\gcd(|a+i|,n)=1$. The predicate holds for every larger $m$ once it holds for $m$, so the declaration states $h(k)\le Ck^2$; it is not vacuous, since $m=0$ fails at $n=1$; counting distinct prime factors is the Formulation of the problem page, and the bound also holds when factors are counted with multiplicity; signed starting points are harmless. The comparator challenge ComparatorChallenges/Jacobsthal.lean, with its configuration ComparatorChallenges/Jacobsthal.json, pins the same statement in the challenge form. The release also proves the stronger declaration erdos_970_iterated_log (the bound displayed above, in Conclusions/IteratedLogBound.lean, challenge ComparatorChallenges/JacobsthalImproved.lean), which would also suffice because $\log\log 3k>0$ for $k\ge1$; this corpus has not built or axiom-checked that declaration, and the accepted claim rests on the quadratic declaration alone.

Acceptance. Formalized: this corpus's verification of 2026-10-07 built the declaration at the pinned revision, found its axiom closure to be exactly propext, Classical.choice and Quot.sound, found the pinned comparator fingerprint identical, and audited the whole statement against the problem's formulation, reading the model file (IsJacobsthalBound, JacobsthalQuadratic), both comparator challenges and QuadraticBound.lean, and checking that no junk value, cast or hidden hypothesis changes the meaning and that these definitions occur nowhere else in the release, its patches or its dependencies. The acceptance is of the Lean statement so audited, which is the displayed question with distinct prime factors and arbitrary starting points; the prose proof of the manuscript was read for its structure only and is not reviewed here. Not reviewed and not refereed: no outside reviewer is known here to have examined the result, the manuscript is a release preprint with no journal record and no arXiv version, and the site's label (OPEN; page accessed, with an empty proof-claim tab) predates the release and does not mention it. The release's own README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification, not all with Lean formalizations.

Depends on. No page of this wiki. The Lean proof depends on Mathlib and on the release's own tree at the pinned revision; the manuscript's prose proof cites a dimension-two fundamental lemma of the sieve, the prime number theorem in progressions, the large sieve, the Weil-type Kloosterman bound and the key renewal theorem, none of which is a page here.