Squarefree numbers in short intervals: explicit and formalized

想象一下数轴是一条向地平线延伸、闪烁着光芒的无尽高速公路。在这条路上，有些数字是“无平方因子”的（squarefree），这意味着它们是由从不重复的独特构建块组成的。可以将它们想象成一套乐高积木，其中没有两块积木的颜色是相同的；你无法用它们搭建出一个完美的正方形塔楼。数学家们早已知晓，如果你观察这段高速公路中极长的一段，这些特殊的数字会以一种可预测的节奏出现，大约每 10 个位置中有 6 个。但如果我们将镜头拉近，观察一段非常短、非常微小的路段呢？这些无平方因子数是否仍能保持它们的节奏，还是会变得混乱且不可预测？这就是“短区间内的无平方因子数”的问题。这是一个数论领域的谜题，数论是研究整数隐藏模式的一个数学分支。解决这个问题有助于我们理解数学的基础结构，就像理解单块砖如何嵌入宏伟的墙壁之中一样。

在这篇论文中，Mayank Pandey 通过将一个已知的数学结果进行“显式化”（explicit）和“形式化”（formalized）处理，来攻克这个谜题。此前，已经有一个结果证明了这些数字在短区间内表现良好，但它依赖于一个强大且复杂的工具（涉及“尼尔序列/nilsequences”以及 Green 和 Tao 的工作），这个工具就像一个黑盒：它告诉我们答案就在那里，但并没有给出计算所需的具体数值。Pandey 的工作就像是将那个黑盒拆解开来，测量内部每一个齿轮和弹簧，并写下它们的精确尺寸。他证明了，如果你选择一个起始点 $X$，且 $X$ 至少大于或等于 $e^{1027/\varepsilon^2}$（这是一个大得惊人的数字），并且观察一个长度为 $H = X^{1/5 - 2/90935 + \varepsilon}$ 的区间，你所找到的无平方因子数的数量将非常接近预期数量。具体而言，实际计数与预期计数之间的差值被保证不会大于 $10450 \varepsilon H X^{-\varepsilon/1025}$。只要区间不是太短且起始数字足够大，这就是一个具体的、可计算的承诺。

为了实现这一点，Pandey 必须在一个棘手的“误差项”（error terms）景观中穿行，这些误差项是计数中的微小波动。他将问题分解成不同的区域。在某些区域，通过使用标准技术（例如通过反复减去差值来平滑波动）可以轻松驯服这些波动。而在其他更困难的区域，波动则非常顽固。在原论文中，这些顽固区域是由前文提到的“黑盒”工具处理的。然而，Pandey 决定亲自进行繁重的体力活。他将数学表达式视为一团纠缠在一起的绳结。他没有使用魔术来解开它，而是仔细地拉动特定的绳索（使用一种称为“范德科皮差分法/van der Corput differencing”的方法）来松开这个结。他证明了即使这些绳索看起来很乱，它们也不会以破坏模式的方式卡住。通过将问题拆分为更小的案例并逐一检查，他证明了对于他所研究的特定范围，这些“波动”小到可以忽略不计。

论文还刻意选择了简化解释以求清晰。虽然计算机代码（在 Lean 4 中形式化）包含了一个稍显优化且更精确的数学版本，但书面笔记呈现的是一个更“粗略”的版本，以便于理解。这就像是给学生展示一张简化的城市地图来教授主要路线，而不是递给他们一张标有每一个小巷的卫星图像。作者指出，这种简化虽然略微削弱了最终的指数，但核心发现依然稳固：无平方因子数的模式即使在非常短的区间内也能保持稳定，而且现在我们有了确切的数字来证明这一点。这项工作是一项严谨的证明，而非猜测或模拟，它证实了即使当我们通过显微镜观察时，数学结构依然如我们所期望的那样井然有序。