🔢 mathematics

Dead ends in square-free digit walks

本文证明了无平方数数字行走中“死胡同”的渐近密度约为 $1.317\times 10^{-9}$ ，这比随机模型预测的数值大约小 40,000 倍，并利用 AxiomProver 系统在 Lean/Mathlib 中完全形式化的结果，建立了所有进制下这些密度的闭式表达式。

原作者： Evan Chen, Chris Cummins, Ben Eltschig, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Aram Markosyan, Ken Ono, Manooshree Patel, Gaurang Pendha

发布于 2026-02-09

📖 1 分钟阅读🧠 深度阅读

CC BY 4.0

原作者： Evan Chen, Chris Cummins, Ben Eltschig, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Aram Markosyan, Ken Ono, Manooshree Patel, Gaurang Pendharkar, Vedant Rathi, Alex Schneidman, Volker Seeker, Shubho Sengupta, Ishan Sinha, Jimmy Xin, Jujian Zhang

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

游戏：“无平方数数字漫步”

想象你正在玩一个关于数字的游戏。你从一个**“无平方数”（square-free）**的数字开始。

什么是无平方数？ 指的是一个因数中不包含任何大于 1 的完全平方数的数字。例如，10 是无平方数（它是 $2 \times 5$ ），但 12 不是（它是 $4 \times 3$ ，而 4 是一个平方数）。
移动规则： 你试图通过在数字末尾逐个添加一位数字来向无穷大“漫步”。如果你现在的数字是 5，你可以尝试把它变成 50, 51, 52, ..., 直到 59。
规则限制： 你创造出的每一个新数字也必须是无平方数。如果你创造了一个不是无平方数的数字，那么这条路径就是“死路”。

核心问题： 你能永远走下去吗？是否存在一个起始数字和一组数字序列，让你能够一直选择下去而永远不会撞到死路，从而实现向无穷大的漫步？

旧有的猜想：“硬币投掷理论”

在此论文之前，数学家们（特别是 Miller 等人）使用一种“随机”模型来研究这个问题。他们把无平方数性质看作是在抛硬币。

大约 60% 的数字是无平方数。
他们设想，每走一步，你都有 60% 的机会找到一个“安全”的数字可以添加。
因为你有 10 个数字可以选择，他们计算出遇到死路（撞到尽头）的概率非常低。
他们的预测： 他们认为死路非常罕见，大约每百万个数字中才会出现 52 次。他们相信无限漫步几乎是必然的。

新的发现：“算术陷阱”

这篇论文证明了“硬币投掷理论”是错误的。数字的真实世界比随机的硬币投掷要顽固得多。

作者们（由人类数学家和名为 AxiomProver 的 AI 工具组成的团队）发现，死路实际上极其罕见——大约为 10 亿分之一。

为什么会有这种差异？
“硬币投掷”模型假设一个数字失败的原因是相互独立的。它认为因为数字 '0' 而失败与因为数字 '1' 而失败之间没有关系。

但在现实中，算术规则创造了一个紧密的陷阱。

类比： 想象你要用 10 把不同的钥匙去锁一扇门。旧理论认为每把钥匙都有 60% 的独立成功率。
现实： 这些“锁”（如质数的平方 $4, 9, 25, 49$）非常挑剔。一个数字要同时对所有 10 个数字都失效，它必须同时满足涉及许多不同质数的、非常特定且复杂的条件。
由于这些条件如此特定且相互关联，想要找到一个让所有可能的下一个数字都失效的数字是非常困难的。这些“死路”如此罕见，以至于随机模型大大高估了它们出现的频率。

结果：一个新的公式

该论文提供了一个精确的数学公式（“闭式表达式”），可以计算出任何进制下（不仅限于十进制）这些死路的精确稀有度。

对于十进制，死路的真实密度大约是 $1.3 \times 10^{-9}$ 。
这比旧有的预测要小约 40,000 倍。

“AI”转折点：AxiomProver

这篇论文的一个独特之处在于其完成数学推导的方式。

作者并没有仅仅靠手工编写证明。他们使用了一个名为 AxiomProver 的 AI 工具。
他们向 AI 输入了一段关于该问题的纯英文描述：“寻找无平方数数字漫步中死路的密度。”
AI 不仅仅是在猜测；它推导出了公式，并用一种叫做 Lean 的计算机语言编写了一个形式化证明。
随后，计算机逐步验证了该证明，以确保其逻辑上是 100% 正确的。
随后，人类作者接过了这个由计算机生成的证明，并撰写了这篇论文，以便向人类解释。

关于历史的说明（“更新”）

论文中包含了一个重要的更新：在发布他们的工作后，他们得知一位名叫 Mirsky 的数学家早在 1947 年就解决了完全相同的问题。

Miller 等人 2024 年的论文（引发“硬币投掷”争论的那篇）忘记引用 Mirsky 1947 年的工作。
因此，虽然这篇论文中的数学是正确的，且 AI 证明是一个很酷的新成就，但其结果本身在数学史上并不是全新的。作者决定不将其发表在学术期刊上，因为答案早已为人所知，但他们分享它是为了展示其 AI 工具重新发现旧数学的能力。

总结

游戏： 你能否通过不断添加数字，在不撞到非无平方数数字的情况下永远走下去？
旧观点： 可以，几乎是肯定的。死路很罕见（两万分之一）。
新观点： 死路极其罕见（十亿分之一），因为数学规则比随机概率更加严格。
方法： 一个名为 AxiomProver 的 AI 工具成功推导并证明了正确的公式，重新发现了被遗忘的 1947 年的研究结果。

技术摘要：无平方数数字游走中的死胡同

问题陈述
本文研究了无平方数数字游走中“死胡同”（dead ends）的存在性及其密度。在基数 $b$ 下的“无平方数游走”始于一个无平方数整数 $N_0$ ，并试图构建一个无限序列 $N_0, N_1, N_2, \dots$ ，其中每一个后续项是通过附加一个数字 $d \in \{0, \dots, b-1\}$ 形成的，即 $N_{k+1} = bN_k + d$ 仍保持为无平方数。

一个正整数 $N$ 被定义为死胡同，如果满足以下条件：

$N$ 是无平方数。
对于基数中的每一个数字 $d$ ，扩展形式 $bN + d$ 都不是无平方数。

Miller 等人 [5] 提出的核心问题是是否存在无限的无平方数游走。虽然一个随机模型（“盲目无限模型”，Blind Unlimited Model）表明无限游走存在的概率接近 1（这意味着在基数 10 中，死胡同的渐近密度约为 $5.218 \times 10^{-5}$ ），但本文通过严谨地分析死胡同的实际算术密度，来确定该随机预测是否成立。

方法论
作者结合了初等乘法数论和包含-排除原理，避免了使用随机模型的概率假设。

指示函数： 该问题利用莫比乌斯函数 $\mu(n)$ 进行重构。由于 $\mu(n)^2$ 是无平方数的指示函数，死胡同 $N$ 的指示函数可以表示为：
$\mathbb{1}_{N \text{ 是死胡同}} = \mu(N)^2 \prod_{d \in D} (1 - \mu(bN + d)^2)$
其中 $D$ 是数字集合。
包含-排除： 该乘积项被展开为对数字集 $S$ 的所有子集的求和。这使得计数函数 $D_b(X)$ （小于等于 $X$ 的死胡同数量）转化为一个关于计数函数 $Q_S(X)$ 的交错和，其中 $Q_S(X)$ 计算的是满足 $n$ 及其扩展 $bn+d $（对于$ d \in S $）均为无平方数的整数$ n \le X$。
筛法分析： 对于固定的子集 $S$ ，通过分析逐个素数来处理 $n$ 及其扩展 $bn+d $为无平方数的条件。作者定义了必须避开的“坏”模$ p^2$ 的剩余类。利用中国剩余定理，他们确定了避开这些剩余类的整数密度。
- 对于大素数 $p$ （其中 $p \nmid b$ ），条件 $p^2 \mid (bn+d)$ 会将 $n$ 限制在模 $p^2$ 的单个剩余类中。至关重要的是，单个素数的平方一次最多只能阻碍一个数字扩展。
- 密度通过包含局部因子 $(1 - \nu_{p,b}(S)/p^2)$ 的无穷乘积（欧拉乘积）来表示，其中 $\nu_{p,b}(S)$ 计算了被禁止的模 $p^2$ 剩余类的数量。
误差项控制： 证明过程仔细界定了由于将筛法截断在参数 $z$ 以及大素数贡献所产生的误差项，建立了 $O(X/\sqrt{\log X})$ 的误差项。

主要结果

定理 1.1（基数 10）： 基数 10 中死胡同的渐近密度存在，并由下式给出：
$c_{\text{dead}} = \sum_{S \subseteq \{0,\dots,9\}} (-1)^{|S|} \prod_{p \text{ prime}} \left( 1 - \frac{\nu_p(S)}{p^2} \right)$
其中 $\nu_p(S)$ 是满足 $p^2 \mid n$ 或对于某个 $d \in S$ 有 $p^2 \mid (10n+d)$ 的 $n \pmod{p^2}$ 剩余类计数。
计算得出的值为 $c_{\text{dead}} \approx 1.317 \times 10^{-9}$ 。
定理 1.2（一般基数 $b$ ）： 该结果可推广到任何基数 $b \ge 2$ 。密度 $c_{\text{dead}}(b)$ 由涉及交错和欧拉乘积的类似闭合形式表达式给出。论文提供了对素数基数 $b \in \{2, 3, 5, 7\}$ 的计算近似值。
与随机模型的差异： 真实的密度（ $\approx 1.3 \times 10^{-9}$ ）比随机预测（ $\approx 5.2 \times 10^{-5}$ ）小了约 40,000 倍。本文将此归因于算术相关性：朴素的随机模型假设数字扩展之间是独立的，但实际上，要求所有十个扩展同时失效，需要由许多不同的素数平方同时进行阻碍，这一条件比独立的概率模型所暗示的条件要严格得多。

意义与主张

结论的解决： 论文证明了虽然随机启发式方法预测无限游走几乎是必然的，但实际的算术结构使得死胡同比预测的要稀有得多。然而，无限游走的存在性仍然是一个开放问题；本文量化了“阻碍”（死胡同）的稀有性，但并未证明无限路径的存在性。
形式化： 论文的一个主要主张是，其主要定理（定理 1.2）已在 Lean/Mathlib 中进行了完全形式化，并且证明是由名为 AxiomProver 的 AI 工具自动生成的。该系统仅被提供了问题的自然语言描述，便自主推导出了闭合形式公式及证明。
历史背景（更新）： 作者指出，在最初发布 arXiv 后，他们得知 Mirsky 在 1947 年 [6] 就已获得了主要结果。论文承认 2024 年 Miller 等人 [5] 的工作未能引用这项先前的工作。因此，虽然 Lean 的形式化是一个有效的自动证明，但作者表示该手稿不会作为主要研究成果提交给期刊发表，而是作为自动定理证明的一个案例研究。

结论
本文对无平方数数字游走中的死胡同密度进行了严谨的算术推导，揭示了由于数论依赖性，其密度与随机预测存在巨大偏差。其最显著的新颖之处在于，如作者所述，其核心贡献在于成功地使用 AxiomProver 完成了该结果的端到端自动形式化，展示了当前 AI 系统处理解析数论中非平凡问题的能力。