短区间中的无平方因子数：显式结果与形式化
Squarefree numbers in short intervals: explicit and formalized
AI总结：
作者将短区间无平方因子数的相关结果显式化并在Lean 4中形式化，给出了特定参数下的误差界，阐述了指数显式化及形式化的相关工作。
AI中文摘要：
本文作者对短区间中的无平方因子数的一项结果进行了显式化与形式化：当0 < ε ≤ 1/90935、X ≥ exp(10²⁷/ε²)且H = X^(1/5 - 2/90935 + ε)时，有|∑_{X≤n≤X+H} μ(n)² - (6/π²)H| ≤ (10⁴⁵⁰/ε) H X^(-ε/10²⁵)。文章阐述了使指数显式化的相关工作，关联的Github仓库包含Lean 4中的形式化内容及该 largely 自动化形式化的相关说明。
英文摘要：
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.
