← All papers
Squarefree numbers in short intervals: explicit and formalized
math.NT
Aug 7, 2026 · v1
TL;DR
Formalizes in Lean 4 an explicit bound on squarefree numbers in short intervals, with largely automated formalization.
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 } μ(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.
Problem
A prior result on the count of squarefree numbers in short intervals was non-explicit. Making the exponent and constants explicit and verifying the result formally were open tasks.
Approach
The known analytic result on squarefree numbers in short intervals is reworked to produce fully explicit constants and exponents. The explicit statement is then formalized in Lean 4. The formalization is described as largely automated, with a GitHub repository documenting the process.
Results
An explicit bound is established: for 0 < ε ≤ 1/90935, X ≥ exp(10^27/ε^2), and H = X^{1/5 - 2/90935 + ε}, the deviation of the squarefree count from (6/π^2)H is bounded by (10^450/ε) H X^{-ε/10^25}. The bound is formally verified in Lean 4.