Erdős Problem #970
Jacobsthal's function
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`IsJacobsthalBound k m` says that every interval of `m` consecutive integers contains an integer coprime to every positive natural number having at most `k` distinct prime factors.
Jacobsthal's function, uniformly parametrized by the maximum number of distinct prime factors.
Let \(h(k)\) be Jacobsthal's function, defined to as the minimal \(m\) such that, if \(n\) has at most \(k\) prime factors, then in any set of \(m\) consecutive integers there exists an integer coprime to \(n\). Determine the order of magnitude of \(h(k)\). In particular, is it true that \[h(k) \ll k^2?\] The bound \(h(k) \ll k^2\) was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof. The order of magnitude of \(h(k)\) remains open.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/970.Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, Jacobsthal: h(k) ≪ k²/(log log 3k)², answering Jacobsthal's h(k) ≪ k² — read by three AI referee seats here 23 Oct, see /day/970-openai-jacobsthal-quadratic-refereed — family 21 at
github.com/openai/math, OpenAI's own Lean proves Theorem 1.1, h(k) ≤ C·k²/(log log 3k)² for every k ≥ 1 (erdos_970_iterated_log), and the quadratic form (erdos_970_quadratic), by the paper's route through the survivor count of Theorem 1.2. Its prime-progression input is not the paper's: both theorems rest on a Lean proof that Landau–Siegel zeros do not exist (dirichlet_real_zero_bound; kernel-checked, unrefereed — see the #431 entry, 23 Oct). Kernel-replayed on our machine on 23 Oct 2026 — 850 modules, 0 errors, standard axioms, both statements and their definitions matched to the comparator challenges under pp.all, leanchecker --fresh rc 0 — after earlier third-party replays (cert-machine 10 Oct with Lean's kernel and nanoda; 30k30, mathvet, nealmcb). Formal Conjectures' two #970 statements and, for #687, Y(x) ≪ x²/(log x · log log x)² follow in kernel-checked bridges — see our /day entry. Bloom calls these claims, not endorsements.
Prizenone
Solution in Leanno
FULL WRITE-UP BY THIS SITE · OCT 23, 2026
Let h(k) − 1 be the longest run of consecutive integers that the multiples of at most k primes can cover. Jacobsthal asked (in a letter Erdős recorded in 1962) whether h(k) ≪ k², and the page asks it in particular; the record since 1978 was Iwaniec's k² log² k. OpenAI's preprint of 25 September (83 pages, family 021) proves h(k) ≪ k²/(log log 3k)², by keeping a classical survivor count alive past sieve parameter 2, where the linear sieve's lower function vanishes. Its Lean (850 modules) was replayed on our box with standard axioms, statements matched, and leanchecker --fresh; about the sixth replay, not the first. Three AI referee seats read §§2–11 and found no gap; one recomputed the decisive margin by a second route (0.147 against the claimed 0.02). Ours: a Lean proof of Y(x) ≪ x²/(log x · log log x)² for Erdős #687, the sharpest form of its o(x²) half that the theorem gives, and Lean proofs of the Formal Conjectures statements that follow (erdos_970 and 687's parts.ii were done first by 30k30; the iterated-log variant, iwaniec and draft PR #7442's quadratic_log are new here). The theorem is OpenAI's.
CLOSED