🔢 mathematics

A Kernel-Checked Exclusion Certificate for Erd\H{o}s Problem 647

本文在 Lean 4 中呈现了一个经过完全验证、公理最小化的证明，通过链接分解因子见证（factorization witnesses），解决了所有 $n > 24$ 至 $10^9$ 范围内的埃尔德什问题 647（Erdős Problem 647），且该结果的可靠性通过在多个独立的工具链和架构上实现字节级一致的复现得到了加强。

原作者： Ibrahim Mian, Shayaan Siddique

发布于 2026-08-19

📖 1 分钟阅读🧠 深度阅读

CC BY 4.0

原作者： Ibrahim Mian, Shayaan Siddique

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

在广袤的数学领域中，有些问题表面上看起来很简单，但在数字的结构内部却隐藏着深刻的复杂性。其中一个问题由传奇数学家保罗·埃尔德什（Paul Erdős）在几十年前提出，涉及一个数字与其约数之间的关系。每个整数都有一组能整除它的较小的数；例如，数字 6 可以被 1、2、3 和 6 整除。这些约数的数量随数字的不同而剧烈变化。埃尔德什想知道，是否存在这样一个特定的模式，即一个数字在约数方面如此“富有”，以至于它能迫使某个特定的数学不等式对所有更大的数字都成立。长期以来，计算机一直在寻找这样的数字，检查了数以十亿计的候选者，但它们只能说：“我们还没有找到。”这些搜索虽然强大，但依赖于标准的计算方法，无法提供绝对的数学确定性，从而留下了一丝怀疑的微光。

一项新的研究终于填补了这个空白，为一大范围的数字提供了结论。它并非通过找到一个解，而是通过证明在特定阈值以下绝对不存在解。研究人员与计算机科学家团队合作，使用了一个专门用于验证数学证明的软件系统，该系统能以人类数学家检查论证每一步骤时的那种严谨性进行验证。他们将重点放在了 25 到 -10 亿之间的数字范围。通过一种将问题分解为数百万个微小且可验证的部分的方法，他们证明了在这个广阔的区间内，埃尔德什描述的情况均不成立。这并非基于数字外观的猜测，也不是来自可能包含隐藏错误的模拟结果。相反，整个推理链条都经过了一个充当公正裁判的计算机程序的检查，确认其逻辑成立，既没有走捷径，也没有未经证实的假设。

这项成就的核心在于研究人员如何处理覆盖如此大范围所需的海量数据。他们并没有试图以一种会耗时永无止境的方式去逐一检查每个数字。相反，他们创建了一个“见证者”（witnesses）链条。想象一下跨越河流的一系列踏脚石：如果你能证明每一块石头都是坚实的，并且相邻两块石头之间的间隙足够小，足以跳过去，那么你就可以横渡整条河而不落水。在这种情况下，“石头”是能够证明不等式在某一整块周围数字范围内失效的特定数字。研究人员生成了超过 600 万个这样的见证者，以覆盖从 25 到 10 亿的整个区间。每一个见证者都是一个经过仔细分析的数字，用以证明它迫使数学条件失效。这项工作的精妙之处在于，计算机验证系统并不仅仅是信任这个见证者列表；它会从头开始重新计算每个见证者的属性，确认它们是有效的，并且能够完美地衔接在一起，不留任何覆盖盲区。

为了确保结果不仅仅是单个潜在有缺陷的计算机程序的产物，团队建立了一套远超标准科学实践的交叉检查系统。他们编写了第二个完全不同的计算机程序，使用不同的语言和不同的方法，来重演整个见证者链条。这个独立的程序检查了每一个步骤，确认了这些数字是有效的，并且逻辑是成立的。此外，他们在不同类型的计算机硬件上，并使用不同的底层软件工具测试了整个过程。他们在不同的机器上从头开始重建了整个系统，确保最终的数字文件在每一位（bit）上都是完全一致的。这种程度的审查意味着，结果并不依赖于特定机器或特定代码的可信度，而是取决于证明本身的根本逻辑。研究人员还回应了之前暗示可能存在解的说法，指出那次早期尝试所使用的逻辑存在一个关键缺陷，而这种新的、严谨的方法规避了该问题。

这项工作的意义不仅在于回答了一个关于数字的具体问题。它展示了一种新的数学研究方式，即结果的可信度是构建在过程之中的。过去，当计算机被用于解决复杂问题时，数学家通常不得不相信计算机没有出错，或者代码没有漏洞。在这里，计算机不仅用于计算，还用于以一种不留疑问的方式验证计算。研究人员证明了，对于 25 到 10 亿之间的每一个数字，埃尔德什描述的条件都不成立。他们并没有找到满足条件的数字，也没有证明在整个数字宇宙中不存在这样的数字。他们只是证明了，如果这样的数字存在，它一定大于 10 亿。这为更广阔、未知的领域留下了可能性，但也为此前仅通过较低确定性方法进行检查的整个范围关上了大门。

该研究还强调了验证所用工具的重要性。研究人员非常谨慎，确保他们的软件不依赖于任何隐藏的假设或未经证实的捷径。他们剥离了流程中任何无法被系统核心逻辑验证的部分。这种方法确保了结果如同其赖以生存的数学基础一样稳固。虽然对于大于 10 亿的数字的搜索仍在继续（其他研究人员正利用不同方法不断推高边界），但这项工作为它所涵盖的范围提供了坚实的确定性。它表明，即使在像数论这样抽象的领域，也是可以搭建起一座逻辑之桥，使其坚固到可以让人充满信心且毫无疑虑地走过。其结果是对一个长期存在的关于特定大规模数字范围问题的清晰、明确的回答，是通过人类洞察力与机器精密度的协作实现的，这为数学研究的可能性树立了新的标准。

技术摘要：针对 Erdős 问题 647 的内核检查排除证书

问题陈述
由 Erdős 和 Selfridge 提出的 Erdős 问题 647 询问是否存在一个整数 $n > 24$ ，使得 $\max_{m<n} (m + \tau(m)) \le n + 2$ ，其中 $\tau(m)$ 是约数计数函数。虽然对于 $n=24$ ，该条件成立且界限 $n+2$ 是紧致的，但据推测不存在进一步的解。此前的计算搜索利用分段筛法和模约减法排除了 $n \approx \dots 18$ 的解，但这些计算依赖于未经验证的代码、原生的 decide 策略或特定问题的公理，因此无法被纳入形式化验证系统的可信证明内核。

方法论与证书设计
本文展示了在 Lean 4 中进行的正式证明，排除了 $24 < n \le 10^9$ 的解。该证明依赖于一种“见证链”（witness-chain）证书格式，旨在让 Lean 内核高效检查，而无需对每个数字进行完整的因数分解。

见证定义： 对于目标 $n$ ，一个“杀伤见证”（kill witness） $m$ 被定义为一个整数，满足 $m < n$ 且 $m + \tau(m) \ge n + 3$ 。此类见证证伪了区间 $[m+1, m + \tau(m) - 3]$ 内所有 $n$ 的不等式。
光滑部分优化： 为了最小化内核工作量，见证并不存储完整的因数分解。相反，它们存储了 $m$ $m$ 被所有素数 $p < 1024$ $p < 1024$ 整除的最大幂次。
- 内核验证这些存储的素数幂之积整除 $m$ 。
- 内核验证每个存储的幂次是极大的（即 $p^{e+1} \nmid m$ ）。
- 内核计算 $\tau(m)$ 的下界为 $\prod (e_i + 1)$ 。
- 倍增规则： 如果 $m$ 的剩余余因子（即不被 $< 1024$ 的素数整除的部分）大于 1，则将该界限翻倍。这是可靠的，因为余因子与光滑部分互质；如果它存在，则至少贡献两个约数（1 和其自身）。
- 所列出的素数（ $< 1024$ ）的素性通过对最多 31 的素数进行试除来验证，无需外部素性证书。
贪婪链构造： 证书是一个通过贪婪算法生成的见证序列。从覆盖位置 24 开始，算法选择一个满足 $m \le C$ 的见证 $m$ ，以最大化新的覆盖位置 $m + \tau(m) - 3$ 。该链包含 6,685,922 个见证，覆盖了整个区间 $(24, 10^9]$ 。
形式化结构： Lean 开发将“正确性层”（证明检查器逻辑的部分）与“数据层”（见证列表）分离。数据被编码为 Lean 源文件中的字面量。内核通过评估这些字面量来验证链的连续性和界限的有效性。

核心贡献与验证
本文提供了五个不同的验证层和贡献点：

公理闭包： 最终定理是在公理集合恰好为 $\{ \text{propext}, \text{Classical.choice}, \text{Quot.sound} \}$ 的情况下证明的。它不包含任何 sorry、native decide 或特定问题的公理。
独立重放： 生成脚本被明确视为不可信。第二个独立的 Python 实现（使用试除法）重放了每一个见证，以验证素性、顺序以及倍增规则。第三个实现独立地重新计算了约数函数，并确认解集与 OEIS A087280 一致。
从源码的可重现性： 在两套独立的 x86 硬件上，通过 gcc 和 clang 从源码编译了 Lean 工具链，并在没有缓存的情况下重建了 mathlib 和开发环境，随后重新生成了证书文件。得到的 .olean 文件与原始 ARM 构建的结果在字节级上完全一致，具有相同的 SHA-256 摘要。
独立检查： 编译后的开发内容通过 lean4checker 进行了重新类型检查，绕过了阐释器（elaborator），从而确认了编译产物的完整性。
对缺陷设计的修正： 本文记录了一次设计迭代，即生成器曾因未能考虑到当大素数（ $>1024$ ）使约数个数减半时应应用倍增规则，导致在“缺口最小值”处停滞。引入“极大性与倍增规则”解决了这一问题，证明了“失败即报错”（fail-loud）生成机制在保持健全性的强化过程中的价值。

结果
主要结果为 定理 1.1：不存在满足 $24 < n \le 10^9$ 的整数 $n$ 使得 $\max_{m<n} (m + \tau(m)) \le n + 2$ 。

该证明使用 6,685,922 个见证覆盖了范围 $(24, 10^9]$ 。
$10^9$ 的证书约为 260 MB 的源代码，作为版本化的发布产物提供。
$10^7$ 和 $10^8$ 的范围通过持续集成进行强制执行； $10^9$ 的范围在 clang 工具链下经过了一次内核检查，并通过独立重放流水线进行了验证。

意义与范围
本文明确指出，它并未解决 Erdős 问题 647，也不声称达到了其他研究者（如 Idén, Hughes, bentrd）的计算前沿（后者已扩展至 $10^{18}$ ）。

信任基础 vs. 范围： 其贡献在于信任基础，而非范围。该结果将非存在性的验证从“未经验证的计算”转移到了“经内核检查的证明”，涵盖范围为 $(24, 10^9]$ 。
有限 vs. 渐近： 本工作处理的是一个特定的间隙——即针对 2026 年 1 月撤回的一项声明。该声明试图通过“支配区间”（domination intervals）覆盖所有 $n > 24$ 来证明该问题，但未能证明这些区间在渐近意义下是重叠的。本文证明了该论证的有限形式（覆盖一个有界范围）是一个可以被内核解决的可检查事实。
未来限制： 作者指出，该方法受限于证书大小和内核时间，而非数学本身。将范围扩展到 $10^{10}$ 将需要约 2 GB 的源代码，而扩展到 $10^{12}$ 则在当前表示法下是不可行的。未来的工作需要通过证明模约减（结构化论证）而非线性见证链来实现。

综上所述，本文建立了一个新的认证搜索标准：一个有限的、完全证明的排除方案，排除了直至 $10^9$ 的解，且仅依赖于 Lean 内核和标准公理，其结果独立于生成器的可靠性。

技术摘要：针对 Erdős 问题 647 的内核检查排除证书

类似论文