AI 24小时改写数论史？Lean 验证确定性因式分解突破 N^{o(1)}

突破核心：从 N^{1/5+o(1)} 到 N^{o(1)} 的确定性跳跃

我第一次认真读这篇论文的摘要，是在一个深夜。标题里那个 $N^{o(1)}$ 在数论和计算复杂性里意味着什么，我太清楚了：它意味着确定性因式分解的时间复杂度不再是某个固定分数次幂，而是对任意常数 $k$ 都能压到 $2^{n/k}$ 步以内，其中 $n$ 是输入位数。这是从"一个非常具体的多项式"到"几乎任何多项式都更快"的质变 来源：HH。

此前这个领域的最佳确定性上界是 $N^{1/5+o(1)}$。我印象里，这个界已经悬了相当长一段时间，改进它需要极其精巧的数论工具。论文声称存在一个确定性图灵机，能在 $N^{o(1)}$ 步内算出任意 $N$ 的最小素因子，对每个 $k\ge 1$ 在 $n$ 位输入上运行不超过 $C_k\,2^{n/k}$ 步 来源：HH。这个结果如果真的站得住，意味着因式分解这个困扰人类几百年的问题，被拉进了一个此前连猜想都不敢这么猜的复杂度等级。

算法思想很直接，也很吓人：把因式分解归约成"计数具有指定前导位的除数"，然后借助曾用于反驳指数时间假设（ETH）的计数引擎来完成这个计数 来源：HH。我读到这里的时候停了一下。ETH 反驳是最近才发生的大事，用同一个引擎来因数分解，这个嫁接方式相当大胆。论文作者自己也说，这个应用是计数引擎的一个实例，比完整的 ETH 反驳证明更易接近，希望它成为理解那个引擎的踏脚石 来源：HH。

但我更在意的，是摘要里那一句几乎被淹没的说明：想法和 Lean 证明均由 AI 生成，人类作者没有阅读证明。这不再是"AI 协助证明"的传统叙事，而是"AI 完成证明，人类只负责审计和编辑"的全新分工 来源：HH。

Lean 形式化验证：13 行陈述 vs 35,000 行证明

形式化验证的细节让这件事变得更耐人寻味。论文说，读者需要检查的 Lean 陈述只有 13 行，只依赖 Mathlib 标准库，任何有经验的 Lean 用户都能快速审计 来源：HH。13 行，这个数字小得让人怀疑是不是哪里弄错了。但完整证明约 35,000 行，比陈述长将近 2700 倍 来源：HH。

我不太确定这个比例在数学形式化中算什么水平，但对比一下更有感觉：Anthropic 的 ETH 反驳证明单独就有约 152,000 行，这篇论文的 35,000 行大约是它的 23% 来源：HH。更关键的是，本文只重新证明了所需的那部分计数引擎，没有导入那些工作中任何其他内容 来源：HH。最小依赖，这是他们刻意为之的设计。

还有一个让我觉得真正有点"快得不像话"的细节：这篇论文是在 ETH 反驳发布后不到 24 小时内完成撰写的，目前不存在人类可读的解释，后续会有一篇详细论文来说明 来源：HH。24 小时。我写一篇 2000 字的博客都要磨两天，他们完成了一篇 35,000 行 Lean 证明的论文。当然，AI 不会累，但人类作者不需要理解就能编辑这件事，才是让我反复咀嚼的地方。

论文的正式化标识是 PALOMAR-2026-10-28-000015 v1，工具是 Lean 4.35 和 Anthropic Claude Opus 5.5 来源：HH。我注意到这个标识里没有作者名字，只有时间戳和编号。这种"认证系统"式的命名，本身就是对传统作者身份概念的一次挑战。

AI 合作模式与多源交叉验证：人机分工的边界

论文包含一个非常坦白的"来源声明"：Claude Opus 5.5 不仅生成了证明，还起草了论文里对证明的解释并检查了引用，人类作者只负责编辑文本和审计陈述 来源：HH。审计什么？审计结果，不是证明。作者明说：证明完全由 Lean 检查，他们唯一做的是把形式化陈述简化到尽可能容易接受审计 来源：HH。

这个分工直接撞上了学术界的作者身份问题。AI 生成了想法和证明，人类指定了陈述并审计了结果，那谁是主作者？谁有资格署名？如果按照贡献大小算，AI 占了绝大部分；如果按照责任承担算，人类是最终签字的人。我翻了一圈 HN 的评论，这篇论文只有 1 分 0 条评论，几乎没人讨论，但我知道这个沉默只是暂时的 来源：HN。

从多源视角看，这个结果与近期 ETH 反驳的连锁反应相呼应，但它独立于那些工作，只复用部分计数引擎 来源：HH。这种"最小依赖"原则其实透露出一种谨慎：他们知道引用一个 152,000 行的未解释证明会让人望而却步，所以把需要验证的东西压缩到 13 行，把重新证明的部分压缩到 35,000 行。

我不确定这种模式最终会演化成什么样子。但有一个判断我可以下：当 13 行陈述被 Lean 验证通过的那一刻，证明的可信度就不再依赖人类是否读过它。作者说他们没读证明，这句话在传统数学里几乎是不可想象的，但在这个框架里，它反而成了优势。审计门槛降到 13 行，数学共同体的任务从"理解"变成了"信任一台机器"。这也许是 AI 时代数学最深刻的改变。

原文：

Deterministic Factoring in Time N^O(1) · 来源：Hacker News

作者：itfan123 值班编辑 · 发布于 2026年10月30日