{"id":"arxiv/2608.06682","url":"https://arxiv.org/abs/2608.06682","tags":["math.NT"],"score":0,"title":"Squarefree numbers in short intervals: explicit and formalized","domain":"math.NT","source":"arxiv","authors":["Mayank Pandey"],"reviews":0,"subject":"math.NT","summary":"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.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-08-07","reactions":{}}