∑math20

Number theory · Result 021

A quadratic bound for Jacobsthal’s function

1 paperLean

Answers Jacobsthal's quadratic-bound question: every interval of \(Ck^2\) consecutive integers contains an integer coprime to any prescribed positive integer with at most k distinct prime divisors, for an absolute constant C. The bound is uniform over prime sets and interval positions and removes the classical logarithmic loss.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of A quadratic bound for Jacobsthal's function

A quadratic bound for Jacobsthal's function

OpenAI · September 25, 2026

Let \(h(k)\) be the least integer such that every interval of \(h(k)\) consecutive integers contains an integer coprime to any prescribed positive integer having at most k distinct prime divisors. We prove \(h(k)\ll k^2/(\log\log(3k))^2\), giving an affirmative answer to Jacobsthal's quadratic-bound question.

Read PDF Download Source

Cite
@misc{OAI:A-quadratic-bound-for-Jacobsthals-function-September-25-2026,
  author = {{OpenAI}},
  title = {{A quadratic bound for Jacobsthal's function}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-quadratic-bound-for-Jacobsthals-function-September-25-2026/paper.pdf}{OAI:A-quadratic-bound-for-Jacobsthals-function-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

Let \(h(k)\) be the least interval length that guarantees an integer coprime to any prescribed positive modulus with at most \(k\) distinct prime factors. The formalization proves the paper's strengthened Jacobsthal bound \(h(k)\le Ck^2/(\log\log(3k))^2\) for one absolute \(C>0\) and every \(k\ge1\). Intervals may begin at any signed integer. The earlier quadratic bound is also retained as a separate statement; the optimal order of growth is not determined.

Comparator links

ResultComparator statement
Quadratic Jacobsthal boundJacobsthal.lean
Jacobsthal bound with an iterated-logarithm savingJacobsthalImproved.lean

Scope note on GitHub →