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<\epsilon \le 1/90935$, $X\ge \exp (10^{27}/{\epsilon }^2)$, $H=X^{1/5-2/90935+\epsilon }$, we have that \[ \biggl|\sum_{X\le n\le X + H } μ(n)^2 - \frac{6}{π^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.

4 pages