An elementary number-theory construction concerning prime-free intervals with prescribed primorial divisibility at the right endpoint, together with a Lean 4 formal verification of the main theorem and infinitude corollary.
Author: Ali Mkhida Affiliation: Algorizk Labs, Bordeaux, France ORCID: 0009-0009-2101-9070
For every prime (p>2), there are infinitely many primes (q) such that
- the open interval ((q,q+p)) contains no prime; and
- (q+p) is divisible by every prime less than (p).
The construction gives an explicit reduced residue class modulo (P\ell), where (P) is the product of the primes below (p) and (\ell>p) is an auxiliary prime. The manuscript also records a positive relative-density lower bound for the constructed family.
docs/paper.pdf— manuscript PDFdocs/paper.tex— LaTeX source
The problem was first studied by the author during a mathematics research internship at the University of Groningen and was later posed publicly on ResearchGate in 2014.
A separate Lean 4 / Mathlib companion verifies the manuscript's main theorem and infinitude corollary.
The positive-relative-density corollary and broader contextual remarks are outside the current formalization scope.
PrimeGapPrimorial.lean— Lean sourcedocs/verification_note.pdf— companion notedocs/verification_note.tex— companion source
git clone https://github.com/qoosmo/PrimeGapPrimorial.git
cd PrimeGapPrimorial
lake exe cache get
lake buildThe Lean/Mathlib environment is pinned by lean-toolchain and
lake-manifest.json.
The Lean source and project configuration are released under the Apache License
2.0 (see LICENSE). The manuscript and companion note are released under
CC BY 4.0.
Ali Mkhida,
"Prime Gaps Ending at Primorial Multiples:
An Explicit Chinese Remainder Theorem Construction,"
manuscript, 2026.