https://openai-aftermath.mathnt.net/index.php?action=history&feed=atom&title=A_quadratic_bound_for_Jacobsthal%27s_function 2026-10-19T00:42:18Z Revision history for this page on the wiki MediaWiki 1.46.2 https://openai-aftermath.mathnt.net/index.php?title=A_quadratic_bound_for_Jacobsthal%27s_function&diff=306&oldid=prev 2026-10-17T18:10:41Z

<p>New page on the quadratic bound for Jacobsthal&#039;s function with the merged Erdős 687 catalogue entry and other public follow-ups</p> <p><b>New page</b></p><div>&#039;&#039;&#039;Jacobsthal&#039;s function&#039;&#039;&#039; &#039;&#039;h&#039;&#039;(&#039;&#039;k&#039;&#039;) is the least integer such that every interval of &#039;&#039;h&#039;&#039;(&#039;&#039;k&#039;&#039;) consecutive integers contains an integer coprime to any given positive integer with at most &#039;&#039;k&#039;&#039; distinct prime divisors. Equivalently, &#039;&#039;h&#039;&#039;(&#039;&#039;k&#039;&#039;) − 1 is the greatest length of an interval that can be covered by one residue class modulo each of &#039;&#039;k&#039;&#039; primes. Jacobsthal asked whether &#039;&#039;h&#039;&#039;(&#039;&#039;k&#039;&#039;) ≪ &#039;&#039;k&#039;&#039;&lt;sup&gt;2&lt;/sup&gt;, and Erdős recorded the question (it is Erdős problem 970). A manuscript dated 25 September 2026 in OpenAI&#039;s public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claims the bound &#039;&#039;h&#039;&#039;(&#039;&#039;k&#039;&#039;) ≪ &#039;&#039;k&#039;&#039;&lt;sup&gt;2&lt;/sup&gt;/(log log 3&#039;&#039;k&#039;&#039;)&lt;sup&gt;2&lt;/sup&gt;. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors&#039; claims; the publication of a paper, code or a formal proof is not presented here as independent verification.<br /> <br /> == Background ==<br /> * As recounted in the introduction of the manuscript:<br /> ** Jacobsthal studied the function from 1960, and Erdős recorded in 1962 Jacobsthal&#039;s question whether &#039;&#039;h&#039;&#039;(&#039;&#039;k&#039;&#039;) ≪ &#039;&#039;k&#039;&#039;&lt;sup&gt;2&lt;/sup&gt;, noting that Brun&#039;s sieve gives a polynomial bound.<br /> ** Iwaniec&#039;s work on the linear sieve gave an estimate of order &#039;&#039;k&#039;&#039;&lt;sup&gt;2&lt;/sup&gt; log&lt;sup&gt;2&lt;/sup&gt; &#039;&#039;k&#039;&#039; when the primes are the first &#039;&#039;k&#039;&#039; primes. Vaughan proved the uniform estimate &#039;&#039;j&#039;&#039;(&#039;&#039;n&#039;&#039;) ≪ ω(&#039;&#039;n&#039;&#039;)&lt;sup&gt;2&lt;/sup&gt;(log 2ω(&#039;&#039;n&#039;&#039;))&lt;sup&gt;4&lt;/sup&gt;, and Iwaniec&#039;s shifted-sieve argument of 1978 gave &#039;&#039;h&#039;&#039;(&#039;&#039;k&#039;&#039;) ≪ &#039;&#039;k&#039;&#039;&lt;sup&gt;2&lt;/sup&gt; log&lt;sup&gt;2&lt;/sup&gt; &#039;&#039;k&#039;&#039; for arbitrary prime sets.<br /> ** 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 &#039;&#039;j&#039;&#039;(&#039;&#039;n&#039;&#039;) ≪&lt;sub&gt;ε&lt;/sub&gt; ω(&#039;&#039;n&#039;&#039;)&lt;sup&gt;1+ε&lt;/sup&gt;.<br /> ** For lower bounds, the long-gap construction of Ford, Green, Konyagin, Maynard and Tao gives &#039;&#039;k&#039;&#039;(log &#039;&#039;k&#039;&#039;)&lt;sup&gt;2&lt;/sup&gt; log log log &#039;&#039;k&#039;&#039;/log log &#039;&#039;k&#039;&#039; for the product of the first &#039;&#039;k&#039;&#039; 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 &#039;&#039;h&#039;&#039;(24) = 236.<br /> <br /> == The original results ==<br /> * &#039;&#039;&#039;A quadratic bound for Jacobsthal&#039;s function (25 September 2026).&#039;&#039;&#039; Theorem 1.1 of the manuscript states that there is an absolute constant &#039;&#039;C&#039;&#039; &gt; 0 with &#039;&#039;h&#039;&#039;(&#039;&#039;k&#039;&#039;) ≤ &#039;&#039;Ck&#039;&#039;&lt;sup&gt;2&lt;/sup&gt;/(log log 3&#039;&#039;k&#039;&#039;)&lt;sup&gt;2&lt;/sup&gt; for every integer &#039;&#039;k&#039;&#039; ≥ 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&#039;s quadratic-bound question; the optimal order of &#039;&#039;h&#039;&#039;(&#039;&#039;k&#039;&#039;) is not determined.<br /> ** &#039;&#039;Method, as described:&#039;&#039; 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.<br /> * &#039;&#039;&#039;Source.&#039;&#039;&#039; Commit &lt;code&gt;1581d4c&lt;/code&gt; 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&#039;s function].<br /> * &#039;&#039;&#039;Formalization, as described by the repository.&#039;&#039;&#039; 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 &#039;&#039;h&#039;&#039;(&#039;&#039;k&#039;&#039;) ≤ &#039;&#039;Ck&#039;&#039;&lt;sup&gt;2&lt;/sup&gt;/(log log 3&#039;&#039;k&#039;&#039;)&lt;sup&gt;2&lt;/sup&gt; for one absolute &#039;&#039;C&#039;&#039; &gt; 0 and every &#039;&#039;k&#039;&#039; ≥ 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].<br /> * &#039;&#039;&#039;Catalogue status.&#039;&#039;&#039; Google DeepMind&#039;s Formal Conjectures project marks &lt;code&gt;erdos_970&lt;/code&gt; and its variant &lt;code&gt;erdos_970.variants.iterated_log&lt;/code&gt; in [https://github.com/google-deepmind/formal-conjectures/blob/7db2ea3b91bfbd0ab620215163e6c488bbb916d5/FormalConjectures/ErdosProblems/970.lean FormalConjectures/ErdosProblems/970.lean] as &quot;research solved&quot;, with &lt;code&gt;formal_proof&lt;/code&gt; links to the openai/math repository; the file states that the order of magnitude of &#039;&#039;h&#039;&#039;(&#039;&#039;k&#039;&#039;) remains open.<br /> <br /> == Public follow-up work ==<br /> {| class=&quot;wikitable&quot;<br /> ! Date !! Work !! Relation !! Public claim !! Public status (checked 18 October 2026)<br /> |-<br /> | 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit &lt;code&gt;c76f1e4&lt;/code&gt;, 14 October 2026) || Review (fidelity of the formal statements) || Rates both challenges &quot;full&quot; 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.<br /> |-<br /> | 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 &lt;code&gt;fd4aeeb&lt;/code&gt;, the journal&#039;s table of exceptions (time-outs, memory, errors) lists neither &lt;code&gt;Jacobsthal&lt;/code&gt; nor &lt;code&gt;JacobsthalImproved&lt;/code&gt;, so both challenges were accepted by con-leche and by Lean&#039;s official kernel. || Development journal.<br /> |-<br /> | 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 &quot;research solved&quot; and links the Lean proofs in the openai/math repository. || Merged.<br /> |-<br /> | 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 &#039;&#039;Y&#039;&#039;(&#039;&#039;x&#039;&#039;) covered by one residue class modulo each prime up to &#039;&#039;x&#039;&#039;, and marks the part &#039;&#039;Y&#039;&#039;(&#039;&#039;x&#039;&#039;) = &#039;&#039;o&#039;&#039;(&#039;&#039;x&#039;&#039;&lt;sup&gt;2&lt;/sup&gt;) as &quot;research solved&quot;, deduced from the bound &#039;&#039;h&#039;&#039;(&#039;&#039;k&#039;&#039;) ≪ &#039;&#039;k&#039;&#039;&lt;sup&gt;2&lt;/sup&gt;, which gives &#039;&#039;Y&#039;&#039;(&#039;&#039;x&#039;&#039;) ≪ &#039;&#039;x&#039;&#039;&lt;sup&gt;2&lt;/sup&gt;/(log &#039;&#039;x&#039;&#039;)&lt;sup&gt;2&lt;/sup&gt;. The &lt;code&gt;formal_proof&lt;/code&gt; 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].<br /> |-<br /> | 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&#039;s open problem 46 on the same covering function as &quot;research solved&quot;, with the bound (&#039;&#039;x&#039;&#039; + 1)&lt;sup&gt;2&lt;/sup&gt;/(log log 3(&#039;&#039;x&#039;&#039; + 1))&lt;sup&gt;2&lt;/sup&gt;. 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.<br /> |-<br /> | 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.<br /> |}<br /> <br /> == Notes ==<br /> * The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.<br /> <br /> [[Category:OpenAI results]]</div>

Aftermath bot