「素数天花板」被 AI 验成：25 岁广州女孩 Axiom Math 把 246 定理机器过一遍

25 岁女孩创业做 AI 数学证明验证，把人类最难的素数定理重新走了一遍。8 月 17 日，由 25 岁广州女孩创立的 Axiom Math 宣布，自家多智能体系统 AxiomProver 完成了「246 素数间隙定理」的 Lean 4 形式化验证，论文挂在 primegaps.axiommath.ai/paper/ 上供公开复核。8 月 22 日新智元把这事单独拎出来写了一篇深度报道，把数学社区推到了「机器可验证」这场 67 年大讨论的风口上。

先说 246 这个数字的份量。孪生素数猜想问的是：是否总能找到两个素数相差 2？比如 3 与 5、11 与 13、17 与 19。19 世纪悬而未决，没人能证。2013 年，张益唐在 58 岁、新罕布什尔大学讲师的位置上，把「存在无穷多对素数差距不超过 7000 万」先证明出来。牛津的 James Maynard 用另一套方法把 7000 万直砸到 600，凭这个拿下 2022 年菲尔兹奖。后来 Maynard 联合菲尔兹奖得主陶哲轩，拉起 Polymath8b 线上协作团，硬把 600 推到 246。从 246 之后再没人能把数字往下挪哪怕一步——Axiom Math 创始数学家 Ken Ono 直接说，「这个定理，就是人类目前对素数理解的天花板」。

那 AxiomProver 到底做了什么？关键要说清一件事：它不是证明定理，而是把人类已经证明的定理用机器再走一遍。具体怎么做？这台「阅卷机器」由四个模块闭环协作：

Auto-formalizer 把论文里那些「显然」「容易验证」的跳步，一步步补全成 Lean 4 代码； Conjecturer 自动生成缺失的中间引理； 核心引擎搜索完整证明路径； Auto-informalizer 反过来把机器证明翻译成人话，方便数学家审核。

整个系统不是把一个定理硬塞进 Lean，而是多智能体接力补全「显然」、生成引理、衔接证明路径、再返读成人话，四个模块缺一不可。

这件事为什么值得专门拎出来讲？因为它在「数学社区怎样消化 AI」这条线上，开了一条非常具体的路。前两天陶哲轩与王虹的对话把这事升级到了哲学层面：AI 出证明太多，数学家读不过来怎么办？陶哲轩给的方向是「送养——证明生成和验证交给 AI，专业阐释和发表再交还给数学家」。AxiomProver 这条管线恰好把「送养」的前半段做实了——尤其是 246 定理这种全人类数学家盯了十几年、跳步无数、AI 没法直接读懂的微妙证明。

但比工程意义更狠的是方法论意义：「AI 验一道人类级定理，整个证明链完整跑通 Lean 4」——这不是某次 demo，而是某一道具体定理被锁死成了可独立验证事实。从今天起，数学共同体争论 AI 证明能否发表时，桌子上多了一份实物证据。陶哲轩可以指着这份证明说，这不是「我用几天时间消化它」的主观感受，而是「Lean 4 编译通过、中间引理补全、Auto-informalizer 翻译回人话我都审过」的可重复操作。

这事也很难。一个经常被跳过的细节是：人类数学家在 246 定理的证明中用了大量「显然」「易见」「this completes the proof」这样的跳步。AxiomProver 要先把每一个「显然」拆成可形式化的子目标，再生成相应引理，最后用核心引擎串起来。这中间任何一个环节断裂，整条验证就作废。这也是为什么 Lean 4 自动形式化被公认为「数学 AI 的硬骨头」——不是模型够大就能过，而是要工程上一个个啃。Ken Ono 肯挂名站台，也是因为这事一旦跑通，意味着 Lean 4 形式化从「个别天才能搞定的极限运动」，开始滑向「常规管线任务」。

下一步最值得看的是几件：

第一，246 定理验证通过只是开始。Axiom Math 接下来如果接连把孪生素数猜想链上的其他里程碑（如 Maynard 2014 的筛法、Goldston-Pintz-Yıldırım 2005 的小间隙）一并形式化，意味着孪生素数猜想的整条递进阶梯会被机器钉死。

第二，Lean 4 自动形式化的「数据-引擎-反馈」飞轮会加速。8 月 19 日 OpenAI 的 Astra 已经用 Lean 4 把 10 道开放定理的证明证书直接写在论文里；Axiom Math 的 AxiomProver 是把「已发表定理的形式化回填」做成流水线。两条路线合流后，数学社区对「AI 辅助论文」的容忍度会快速抬高。

第三，那道「数学家还需要做什么」的问题，迟早要正面回答。陶哲轩刚 ICM 演讲上问过：「如果答案可以被 AI 批量生产，数学研究究竟还要追求什么？」Axiom Math 这种「非证明、只验证」的工具，反而给了一个提示：未来数学家最稀缺的不是解题能力，而是选择哪些问题值得被形式化、怎样把形式化结果反馈回主流期刊的判断能力。

简单说：8 月 22 日不是「AI 又证了一道题」的故事，而是「AI 把人类最难的素数定理完整跑了一遍 Lean 4 验证」的故事。前者只是又一次 demo，后者是数学共同体的判断标尺动了一次。从今天起，「Lean 4 通过 / 不通过」会成为比期刊同行评议更冷静的一种验收姿势。