A quadratic bound for Jacobsthal's function

Jacobsthal's function h(k) is the least integer such that every interval of h(k) consecutive integers contains an integer coprime to any given positive integer with at most k distinct prime divisors. Equivalently, h(k) − 1 is the greatest length of an interval that can be covered by one residue class modulo each of k primes. Jacobsthal asked whether h(k) ≪ k², and Erdős recorded the question (it is Erdős problem 970). A manuscript dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the bound h(k) ≪ k²/(log log 3k)². This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

As recounted in the introduction of the manuscript:
- Jacobsthal studied the function from 1960, and Erdős recorded in 1962 Jacobsthal's question whether h(k) ≪ k², noting that Brun's sieve gives a polynomial bound.
- Iwaniec's work on the linear sieve gave an estimate of order k² log² k when the primes are the first k primes. Vaughan proved the uniform estimate j(n) ≪ ω(n)²(log 2ω(n))⁴, and Iwaniec's shifted-sieve argument of 1978 gave h(k) ≪ k² log² k for arbitrary prime sets.
- Vaughan explained the exponent 2 by the restriction of the one-dimensional sieve to moduli near the square root of the interval length, and suggested the stronger estimate j(n) ≪_ε ω(n)^1+ε.
- For lower bounds, the long-gap construction of Ford, Green, Konyagin, Maynard and Tao gives k(log k)² log log log k/log log k for the product of the first k primes. Hajdu and Saradha showed that this primorial need not be extremal: the value at the product of the first 24 primes is 234, while h(24) = 236.

The original results

A quadratic bound for Jacobsthal's function (25 September 2026). Theorem 1.1 of the manuscript states that there is an absolute constant C > 0 with h(k) ≤ Ck²/(log log 3k)² for every integer k ≥ 1. The bound is uniform over prime sets and interval positions, and the constant is not made explicit. The manuscript describes this as an affirmative answer to Jacobsthal's quadratic-bound question; the optimal order of h(k) is not determined.
- Method, as described: the proof works with one prescribed residue class at each prime below a cutoff. It reaches the limiting parameter of the linear sieve, keeping a boundary contribution that disappears from the leading term. An inverse estimate and stopped counts then control the discrepancy between this reference calculation and the actual prescribed classes.
Source. Commit 1581d4c of the openai/math repository, folder A quadratic bound for Jacobsthal's function.
Formalization, as described by the repository. The scope note lean/docs/021.md states that the formalization proves the bound h(k) ≤ Ck²/(log log 3k)² for one absolute C > 0 and every k ≥ 1, with intervals beginning at any integer, and keeps the quadratic bound as a separate statement. Its Comparator challenges are Jacobsthal.lean and JacobsthalImproved.lean.
Catalogue status. Google DeepMind's Formal Conjectures project marks erdos_970 and its variant erdos_970.variants.iterated_log in FormalConjectures/ErdosProblems/970.lean as "research solved", with formal_proof links to the openai/math repository; the file states that the order of magnitude of h(k) remains open.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 18 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit `c76f1e4`, 14 October 2026)	Review (fidelity of the formal statements)	Rates both challenges "full" and notes that the quadratic and the improved bound are stated with elementary definitions.	MathVet states that it does not claim any theorem false; its tables record no machine check for these two challenges.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit `fd4aeeb`, the journal's table of exceptions (time-outs, memory, errors) lists neither `Jacobsthal` nor `JacobsthalImproved`, so both challenges were accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-11	Formal Conjectures pull request #6898	Catalogue (formal statement)	Marks Erdős problem 970 and its iterated-logarithm variant as "research solved" and links the Lean proofs in the openai/math repository.	Merged.
2026-10-05 (merged 2026-10-17)	Formal Conjectures pull request #6864	Use (catalogue)	Adds Erdős problem 687 on the largest interval Y(x) covered by one residue class modulo each prime up to x, and marks the part Y(x) = o(x²) as "research solved", deduced from the bound h(k) ≪ k², which gives Y(x) ≪ x²/(log x)². The `formal_proof` link points to a Lean derivation by the GitHub user 30k30 in 30k30/scholia. The stronger parts of the problem stay open.	Merged on 17 October 2026, as FormalConjectures/ErdosProblems/687.lean.
2026-10-11	Formal Conjectures pull request #7183 (30k30)	Use (Lean)	Marks the upper-bound part of Ben Green's open problem 46 on the same covering function as "research solved", with the bound (x + 1)²/(log log 3(x + 1))². The linked Lean declaration in 30k30/scholia derives it by the Chinese remainder theorem from the iterated-logarithm theorem in the openai/math repository, and the pull request also corrects the attribution of the lower bound. The description states that the Lean bridge was written with Claude.	Open.
2026-10-14	M. Kripner, V. Rozhoň, R. Šámal, M. Šindelář, A. Zámečník, Hexagon 2610.00239v1, titled Small witnesses for eventual Erdős–Straus binomial divisibility	Remark	The note cites Theorem 1.1 of the manuscript as the nearest sieve problem to its own and states that no Jacobsthal estimate is used as an input.	Hexagon version 1.

Notes

The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.