9月4日，AI for Math公司Axiom Math宣布，在有界素数间隔问题上，将这一上界进一步推进到212——即证明，存在无穷多对相邻素数，它们之间的距离不超过212。
实现这一突破的，是一支兼具顶级数学背景与AI基础设施实力的跨界团队。Axiom成立于2025年，创始人是洪乐潼，毕业于MIT数学与物理专业，曾获 Rhodes Scholar，并进入斯坦福攻读数学博士，她创办Axiom时只有24岁。CTO Shubho Sengupta曾在Meta FAIR工作八年，长期负责大规模AI训练与研究基础设施；首席数学家Ken Ono是国际顶尖的数论学家，AI研究负责人François Charton此前在Meta从事机器学习与数学推理研究，开创性地使用Transformer 架构去解决高阶数学与符号计算难题。
一个十余年几乎没有松动的纪录，突然在几天之内连续变化。此前，Julia Stadlmann刚刚将保持多年的素数间隔从246推进到240；随后，Axiom又借助 AI驱动的搜索、计算与验证，把这一数字进一步压到212。而就在Axiom宣布 212后不久，OpenAI又公开了一套关于素数间隔186的结果。
短短几天里，素数间隔问题突然进入了一轮由AI加速的密集突破期。
Axiom团队告诉ZP，Axiom和OpenAI在“做数学”的基本方法上很可能是相似的：都通过Agent提出证明策略和优化方案，再用Python和Lean进行验证。不同之处在于，Axiom更强调数学表达本身的质量，包括人类可读的非形式化论文，以及高质量的Lean形式化证明。Axiom还提到，OpenAI在这次结果的形式化过程中使用了其PrimeGapsLib。
Axiom此次发的新论文 链接：
https://primegaps.axiommath.ai/bgp212.pdf
而在这轮快速推进之前，关于素数间隔的上一项公认纪录246，已经保持了十余年。
2013年，张益唐首次证明，相邻素数之间存在一个固定的有限上界，将此前“是否存在有限上界”的问题推进到7000万。随后，牛津大学数学家James Maynard 提出一套不同的筛法，将这一上界大幅降至600。这项工作也成为他后来获得 2022年菲尔兹奖的重要研究贡献之一。在此基础上，Maynard、陶哲轩以及一批数论学家通过Polymath8b协作项目继续优化，最终将数字推进到246。此后十余年，这一纪录几乎没有再发生变化。
Axiom CTO Shubho Sengupta在宣布这一结果时写道：“我们正在推动数学的边界。我们把素数间隔降低到了212——这是建立在该领域最新工作的基础之上的。”
这并不是一次传统意义上依靠少数数学家纸笔推演完成的证明。Axiom向ZP透露，这并不是几位数学家坐在办公室里靠纸笔完成的一次传统证明。参与项目的是一支混合团队：数论学家、应用数学家、工程师，以及AxiomProver。
论文明确写道，212背后的核心解析思想来自Stadlmann，Axiom团队在分布式计算集群上进行了大规模数值实验，对不同解析估计、积分区域和参数组合反复优化，主要强化了三处关键环节。第一，不再过早把复杂条件简化成统一的充分条件；第二，不再只检查最坏情况，而是在连续参数空间里逐一验证；第三，补上了x1/2附近原本最棘手的“过渡区”。这些改进扩大了筛法真正可利用的参数空间。再配合对参数与变分问题的持续优化，团队最终让关键指标越过证明所需的临界值，并找到一组直径为212的45元admissible tuple，由此得到新的结果
Shubho透露，这项工作的内部代号是一个只有大约六个人知晓的“Skunkworks”项目。整个项目持续约两周。一次完整的数值实验大约需要六天。工程团队随后通过大规模并行化、预计算以及更高效的特征值求解方法，将一次实验压缩到了几个小时。
212并不是Axiom最近第一次因为素数间隔进入公众视野。就在几周前，这家公司刚刚完成了另一项与246有关的工作：让AxiomProver对“素数间隔不超过 246”这一结果完成大规模Lean形式化。
Axiom的结果公布后，很快引发了数学界和科技圈的讨论。
文艺复兴科技B Capital Group董事长Howard Morgan转发相关进展时写道：“这是这家公司一个重要的成果。不确定大家是否已经准备好让计算机去拿菲尔兹奖，不过这个AI倒确实还不到40岁:)”
另一位研究者Andrew M. Dai则评价：“Axiom又做出了令人难以置信的数学工作，此前相关方向的成果曾催生菲尔兹奖级别的研究。”
曾经发表过多篇素数间隔论文的数学研究者Lola Thompson在看到结果后写了一段颇为复杂的话：几天前，她还因为Julia Stadlmann推进这一问题而感到非常兴奋——那是自2014年以来该界第一次出现重要改进。但随后，Stadlmann的结果在同一天先后被Axiom和ChatGPT超越。
她写道：“这一切让我开始怀疑，我为什么还在做数学研究。还有意义吗？数学家是不是正在变得过时？”她也承认，一种合理的反驳是：AI的成果仍然大量建立在人类数学家Julia的工作之上，因此人类当然依然重要。
“即便如此，看到 AI 如此迅速地超过我们，我还是觉得非常泄气。”这可能比AI 会不会拿菲尔兹奖更接近今天数学界真正面对的问题。
当然，从186到孪生素数猜想要求的2，中间仍然隔着巨大的理论鸿沟。Axiom 团队认为：“相比212这个数字，更值得关注的是AI正把改变数学研究的范式——人类负责提出真正重要的问题与方向，AI则用更强的搜索、计算和验证能力不断放大这种创造力。”
212、186，或许都还只是这套新研究方式留下的早期刻度。真正值得想象的是，但如果这套范式继续演进，未来数学突破的基本单元，或许将不再只属于某位天才数学家的灵光一瞬，而是一场人与AI的双重奏。
以下是ZP和Axiom团队的独家对话实录，经编辑翻译，enjoy~
01 从形式化到自主证明，谁在定义 AI 做数学的方式？
ZP：为什么“不要过早简化条件”如此重要？这会不会成为AI做数学时的一种常见方法？
Axiom：这里其实存在一个非常微妙的平衡：一方面要去掉那些与证明无关、多余的条件，另一方面又必须保留证明真正需要的条件。
形式化证明的优势就在于，它为AI系统提供了一个非常理想的基础环境，使AI 能够在证明的每一步中，对这些条件做出判断。
ZP：论文中提到，AxiomProver“自主生成了一个Lean证书”。这里的“自主”究竟到了什么程度？
Axiom：我们把论文交给AxiomProver，让它基于已有文献，对论文中的主要结果进行形式化，同时以此前我们对“246定理”的形式化工作为基础。在此之后，没有任何进一步的人工参与。
ZP：那么在整个过程中，哪些环节实际上仍然需要人工介入？
Axiom：在形式化证明这个环节本身，并不需要人工干预。
但设计计算基础设施中人类需要发挥关键作用，我们会高效地对Stadlmann的工作进行迭代和优化。
ZP：目前关于 212 这个界的 Lean 形式化，是从最底层的基础公理开始的吗？
Axiom：目前的Lean形式化仍然是建立在已有文献基础之上的。不过 AxiomProver也正在继续把这些依赖的结果形式化。
ZP：如果把 212 这个结果背后的定理依赖一层层向下追溯，要实现真正端到端的形式化，目前还缺哪些部分？
Axiom：Stadlmann证明中的一个关键步骤，是使用了基于Bombieri–Vinogradov定理的五种不同解析估计，而此前的证明只使用其中一种。
这五种解析估计，是目前仍然需要进一步形式化的主要输入。
ZP：为什么这些部分在现阶段尤其难处理？
Axiom：我们认为没有什么形式化任务是AxiomProver无法完成的，区别只在于需要多少时间。
ZP：OpenAI最近宣布，GPT-6 Astra也在研究有界素数间隔，并将界推进到了 186。你们怎么看这件事？这个时间点只是巧合吗？
Axiom：数学中这样一个最基础、也最优美的问题吸引其他公司的兴趣，这并不意外。现在有很多团队都在积极研究这个问题。我们欢迎竞争。
ZP：你认为双方“做数学”的基本方法是一样的吗？
Axiom：如果说的是使用Agent提出证明策略和优化方案，并使用Python和Lean对这些方案进行验证，那么双方的方法很可能是相似的。
不过，在Axiom，我们非常强调数学沟通本身的质量。这既包括写出人类能够清晰阅读的非形式化论文，也包括生成高质量的Lean形式化证明。
OpenAI在他们这次结果的形式化过程中使用了我们的PrimeGapsLib，这也反映了我们Lean代码的质量。
ZP：你怎么看通用前沿模型与专门做 AI for Math 的公司，两者各自的价值？
Axiom：前沿模型的能力正在越来越强，但运行成本也非常高。
Axiom已经证明，围绕形式化证明构建定制化的工具、harness 和模型，可以在速度、效率以及质量上带来显著提升。
这些因素对于大规模开展形式化工作非常关键，尤其是在未来，大多数研究论文和大部分代码可能都不会再由人类亲自阅读。
02 6个人两周内进行的秘密项目：212背后的工程化数学实验
ZP：参与这个项目的六名团队成员分别是什么背景？大家是如何分工的？
Axiom：我们的团队由数学家和工程师组成。
数学家主要负责利用Agent工作流，探索可能降低这个距离的策略。
工程师则负责搭建高效、经过优化的计算基础设施，让团队能够快速迭代各种潜在思路。
<