Squarefree numbers in short intervals: explicit and formalized
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.
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2608.06682
curl -X POST /api/v1/records/arxiv/2608.06682/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2608.06682/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'