A squarefree number is a positive integer that is not divisible by any perfect square other than 1. For example, 6 is squarefree but 12 is not, because 12 is divisible by 4. It is a classical fact that roughly 61 percent of all integers are squarefree (specifically, the fraction is 6 divided by pi squared). A natural question is whether this proportion holds not just over all integers up to some large number X, but also within short stretches of consecutive integers near X. This paper gives a precise, fully explicit answer to that question.
The main result is a concrete inequality showing that within an interval of length H starting near X, the count of squarefree numbers is very close to what the 61 percent estimate would predict. Previous work by the same author had established that such a result holds in principle, but with unspecified constants buried inside the proof. Here, every constant is pinned down to an actual number, no matter how large or unwieldy. The interval length H can be as short as roughly X to the power of one-fifth, which is much shorter than X itself, and the error between the actual count and the prediction is shown to be rigorously bounded.
Making everything explicit required carefully tracking hundreds of estimates throughout a long and technical proof, a process that is tedious and error-prone when done by hand. To address this, the authors also formalized the entire proof using Lean 4, a computer proof assistant that mechanically checks every logical step. Much of this formalization was carried out in a largely automated way. The result is both a human-readable account of where all the explicit constants come from and a machine-verified certificate that the proof is correct, representing a combination of classical analytic number theory and modern formal verification.