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工作流，探索可能降低这个距离的策略。

工程师则负责搭建高效、经过优化的计算基础设施，让团队能够快速迭代各种潜在思路。

ZP：一开始，每次实验大约需要六天，后来被压缩到了几个小时。单次实验的输入和输出分别是什么？具体做了哪些工程优化？

Axiom：输入包括对解析估计方法的具体选择、积分区域，以及其他参数。输出始终只有一个数字，也就是一对矩阵的广义特征值。如果想要得到一个更小的界，就意味着这个特征值必须越过一个预先设定的阈值。

工程优化本质上主要包括几个方面：大规模并行化、预计算，以及用于高效计算特征值的高级数值方法。

ZP：有没有某一个明确的瞬间，让你们意识到“纪录真的被打破了”？当时机器输出了什么？

Axiom：有。当我们某一组参数对应的特征值输出越过那个阈值时，我们就知道成功了。

ZP：在这两周里，你们还尝试了哪些验证实验？失败了多少次？

Axiom：我们绝大多数实验都失败了，其中有一些距离阈值其实只差非常小的一点。

整个过程中最重要的杠杆，是如何选择解析估计。事实证明，Stadlmann所使用的五种估计的特定组合，是其中一个非常关键的因素。

ZP：能否举一个具体例子，说明某个关键突破是如何由两种不同研究能力碰撞出来的？

Axiom：我们的一位数学家在量化行业有过经验，所以他能够大幅提高我们的优化pipeline的效率；我们的一位工程师拥有数论博士学位，因此他既能够参与想法生成，也能够参与具体实现。

03 212之外：数学研究的时间尺度正在改变

ZP：在选择问题时，“这个问题是否适合AI”会成为一个标准吗？还是问题本身的重要性才是决定因素？

Axiom：我们之所以选择降低素数间隔的界，是因为我们认为这个问题非常优美，也很有意思。

一开始，我们其实并不知道要实现这个目标究竟需要做什么。

结果证明，这恰好是一个非常适合这种由AI驱动的新型数学研究方法的问题。

ZP：张益唐曾经说过，从7000万到246，本质上只是“从有限到有限”。那么你怎么看从240到212？AI在这两类问题中的价值分别是什么？

Axiom：从240推进到212所需要的这种优化工作，恰恰是非常适合AI系统完成的任务。

这代表了一种新的数学研究范式：人类的创造力可以通过AI强大的计算和搜索能力得到增强，并进一步被完善。

从长期来看，我们完全相信，AI系统最终能够完成那些真正需要更深层突破的问题，包括最终解决双生素数猜想这样的难题，但达到那个阶段还有很长的路。

ZP：这次真正的里程碑究竟是什么：212这个数字本身，还是得到它的研究工作流？

Axiom：几乎可以肯定是研究工作流本身。

AI驱动的证明提炼和优化，是我们正在Axiom构建的核心能力之一。

而有界素数间隔这样的问题，对我们来说恰好是非常理想的试验场，可以帮助我们打造未来数学研究所需要的工具。

ZP：你们内部把这项工作概括为“一种新的做数学方式”。你会如何定义这种新范式？究竟发生了什么变化？

Axiom：过去，数学研究往往是一个相当艰苦而漫长的过程。人类可能需要花几个月时间提出和讨论想法，再用几年时间完成论文。

如果是在AI之前的时代，即使我们以极快的速度工作，这个项目也很容易需要几个月才能完成。AI让我们可以以前所未有的速度生成、筛选、测试和迭代数学想法，这显著加快了我们开展数学研究的能力。

请注意，本次访谈内容已经过编辑整理并已获得Axiom团队的认可，仅代表受访者个人观点。欢迎读者通过留言互动，分享您对本访谈的看法。Z Potentials 将继续提供更多关于人工智能、全球化市场、机器人技术等领域的创业者访谈。我们诚邀对未来充满憧憬的您加入我们的社群，与我们共同分享、学习、成长。