Oct 6, 2026
Lean formalization in OpenAI math repository (Result 021)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A quadratic bound for Jacobsthal's function'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 021). The Lean development was not rebuilt locally.