Squarefree numbers in short intervals: explicit and formalized

Imagine the number line as an endless, shimmering highway stretching into the horizon. On this road, some numbers are "squarefree," meaning they are built from unique building blocks that never repeat. Think of them as a set of LEGO bricks where no two pieces are the same color; you can't build a perfect square tower with them. Mathematicians have long known that if you look at a huge stretch of this highway, these special numbers appear with a predictable rhythm, roughly 6 out of every 10 spots. But what happens if you zoom in and look at a very short, tiny stretch of the road? Do the squarefree numbers still keep their rhythm, or do they get chaotic and unpredictable? This is the question of "squarefree numbers in short intervals." It's a puzzle in the field of number theory, a branch of math that studies the hidden patterns of whole numbers. Solving it helps us understand the fundamental structure of mathematics, much like understanding how a single brick fits into a massive wall.

In this paper, Mayank Pandey tackles this puzzle by taking a known mathematical result and making it "explicit" and "formalized." Previously, a result existed that proved these numbers behave well in short intervals, but it relied on a powerful, complex tool (involving "nilsequences" and work by Green and Tao) that acted like a black box: it said the answer was there, but it didn't give the specific numbers needed to calculate it. Pandey's work is like taking that black box apart, measuring every gear and spring inside, and writing down the exact dimensions. He proves that if you pick a starting point $X$ that is at least as big as $e^{1027/\varepsilon^2}$ (a staggeringly large number) and look at an interval of length $H = X^{1/5 - 2/90935 + \varepsilon}$, the number of squarefree numbers you find will be very close to the expected amount. Specifically, the difference between the actual count and the expected count is guaranteed to be no larger than $10450 \varepsilon H X^{-\varepsilon/1025}$. This is a concrete, calculable promise, provided the interval isn't too short and the starting number is huge enough.

To achieve this, Pandey had to navigate a tricky landscape of "error terms," which are the little wobbles in the count. He breaks the problem down into different zones. In some zones, the wobbles are easy to tame using standard techniques, like repeatedly subtracting differences to smooth out the bumps. In other, more difficult zones, the wobbles are stubborn. In the original paper, these stubborn zones were handled by the "black box" tool mentioned earlier. Pandey, however, decided to do the heavy lifting manually. He treats the mathematical expressions like a tangled knot of strings. Instead of using a magic trick to untie it, he carefully pulls on specific strands (using a method called "van der Corput differencing") to loosen the knot. He shows that even though the strings look messy, they don't get stuck in a way that ruins the pattern. By splitting the problem into smaller cases and checking them one by one, he proves that the "wobbles" are small enough to be ignored for his specific range.

The paper also makes a deliberate choice to simplify the explanation for the sake of clarity. While the computer code (formalized in Lean 4) contains a slightly more optimized and precise version of the math, the written note presents a "rougher" version that is easier to follow. It's like showing a student a simplified map of a city to teach them the main routes, rather than handing them a satellite image with every single alleyway marked. The author notes that this simplification does weaken the final exponent slightly, but the core finding remains solid: the pattern of squarefree numbers holds up even in very short intervals, and now we have the exact numbers to prove it. The work is a rigorous proof, not a guess or a simulation, confirming that the mathematical structure is as orderly as we hoped, even when we look at it through a microscope.