View source for 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''<sup>2</sup>, and Erdős recorded the question (it is Erdős problem 970). A manuscript dated 25 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claims the bound ''h''(''k'') ≪ ''k''<sup>2</sup>/(log log 3''k'')<sup>2</sup>. 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''<sup>2</sup>, noting that Brun's sieve gives a polynomial bound.
** Iwaniec's work on the linear sieve gave an estimate of order ''k''<sup>2</sup> log<sup>2</sup> ''k'' when the primes are the first ''k'' primes. Vaughan proved the uniform estimate ''j''(''n'') ≪ ω(''n'')<sup>2</sup>(log 2ω(''n''))<sup>4</sup>, and Iwaniec's shifted-sieve argument of 1978 gave ''h''(''k'') ≪ ''k''<sup>2</sup> log<sup>2</sup> ''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'') ≪<sub>ε</sub> ω(''n'')<sup>1+ε</sup>.
** For lower bounds, the long-gap construction of Ford, Green, Konyagin, Maynard and Tao gives ''k''(log ''k'')<sup>2</sup> 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''<sup>2</sup>/(log log 3''k'')<sup>2</sup> 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 <code>1581d4c</code> of the openai/math repository, folder [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-quadratic-bound-for-Jacobsthals-function-September-25-2026 A quadratic bound for Jacobsthal's function].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/021.md lean/docs/021.md] states that the formalization proves the bound ''h''(''k'') ≤ ''Ck''<sup>2</sup>/(log log 3''k'')<sup>2</sup> 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/Jacobsthal.lean Jacobsthal.lean] and [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/JacobsthalImproved.lean JacobsthalImproved.lean].
* '''Catalogue status.''' Google DeepMind's Formal Conjectures project marks <code>erdos_970</code> and its variant <code>erdos_970.variants.iterated_log</code> in [https://github.com/google-deepmind/formal-conjectures/blob/7db2ea3b91bfbd0ab620215163e6c488bbb916d5/FormalConjectures/ErdosProblems/970.lean FormalConjectures/ErdosProblems/970.lean] as "research solved", with <code>formal_proof</code> links to the openai/math repository; the file states that the order of magnitude of ''h''(''k'') remains open.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 18 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) lists neither <code>Jacobsthal</code> nor <code>JacobsthalImproved</code>, so both challenges were accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-11 || [https://github.com/google-deepmind/formal-conjectures/pull/6898 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) || [https://github.com/google-deepmind/formal-conjectures/pull/6864 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''<sup>2</sup>) as "research solved", deduced from the bound ''h''(''k'') ≪ ''k''<sup>2</sup>, which gives ''Y''(''x'') ≪ ''x''<sup>2</sup>/(log ''x'')<sup>2</sup>. The <code>formal_proof</code> link points to a Lean derivation by the GitHub user 30k30 in [https://github.com/30k30/scholia/tree/b072c89c3edac06521868e32cc15b2bc91bd8533/erdos-687 30k30/scholia]. The stronger parts of the problem stay open. || Merged on 17 October 2026, as [https://github.com/google-deepmind/formal-conjectures/blob/a469aaa0bceabd4b909dad06141053675455af94/FormalConjectures/ErdosProblems/687.lean FormalConjectures/ErdosProblems/687.lean].
|-
| 2026-10-11 || [https://github.com/google-deepmind/formal-conjectures/pull/7183 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)<sup>2</sup>/(log log 3(''x'' + 1))<sup>2</sup>. 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, [https://hexagonmath.org/2610.00239v1 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.

[[Category:OpenAI results]]