arXiv · 2608.06682
Squarefree numbers in short intervals: explicit and formalized
Abstract
We make explicit and formalize a result of the author on squarefree numbers in short intervals, showing that for $0 < \varepsilon\le 1/90935 $, $X\ge \exp(10^{27}/\varepsilon^2)$, $H = X^{1/5 - 2/90935 + \varepsilon}$, we have that \[ \biggl|\sum_{X\le n\le X + H } \mu(n)^2 - \frac{6}{\pi^2}H\biggr| \le \frac{10^{450}}{\varepsilon} H X^{-\varepsilon/10^{25}}. \] This article gives an account of what went into making the exponent explicit. The Github repository linked contains the formalization in Lean 4 as well as an account of what went into the largely automated formalization.
Explore related subjects
Keep this discovery
Mayank Pandey. 2026-08-07. Squarefree numbers in short intervals: explicit and formalized. https://arxiv.org/abs/2608.06682
Cite the original work for its findings. Save a collection to share your selection of sources.