独家｜对话硅谷独角兽Axiom：00后创始人，6个人、两周秘密实验，AI如何打破十年素数间隔问题纪录？

Axiom团队告诉ZP，Axiom和OpenAI在“做数学”的基本方法上很可能是相似的：都通过Agent提出证明策略和优化方案，再用Python和Lean进行验证。不同之处在于，Axiom更强调数学表达本身的质量，包括人类可读的非形式化论文，以及高质量的Lean形式化证明。Axiom还提到，OpenAI在这次结果的形式化过程中使用了其PrimeGapsLib。

而在这轮快速推进之前，关于素数间隔的上一项公认纪录246，已经保持了十余年。

这并不是一次传统意义上依靠少数数学家纸笔推演完成的证明。Axiom向ZP透露，这并不是几位数学家坐在办公室里靠纸笔完成的一次传统证明。参与项目的是一支混合团队：数论学家、应用数学家、工程师，以及AxiomProver。

212并不是Axiom最近第一次因为素数间隔进入公众视野。就在几周前，这家公司刚刚完成了另一项与246有关的工作：让AxiomProver对“素数间隔不超过 246”这一结果完成大规模Lean形式化。

ZP：为什么“不要过早简化条件”如此重要？这会不会成为AI做数学时的一种常见方法？

Axiom：这里其实存在一个非常微妙的平衡：一方面要去掉那些与证明无关、多余的条件，另一方面又必须保留证明真正需要的条件。

ZP：论文中提到，AxiomProver“自主生成了一个Lean证书”。这里的“自主”究竟到了什么程度？

Axiom：我们把论文交给AxiomProver，让它基于已有文献，对论文中的主要结果进行形式化，同时以此前我们对“246定理”的形式化工作为基础。在此之后，没有任何进一步的人工参与。

ZP：那么在整个过程中，哪些环节实际上仍然需要人工介入？

Axiom：在形式化证明这个环节本身，并不需要人工干预。

ZP：目前关于 212 这个界的 Lean 形式化，是从最底层的基础公理开始的吗？

Axiom：目前的Lean形式化仍然是建立在已有文献基础之上的。不过 AxiomProver也正在继续把这些依赖的结果形式化。

ZP：如果把 212 这个结果背后的定理依赖一层层向下追溯，要实现真正端到端的形式化，目前还缺哪些部分？

ZP：为什么这些部分在现阶段尤其难处理？

ZP：你认为双方“做数学”的基本方法是一样的吗？

Axiom：如果说的是使用Agent提出证明策略和优化方案，并使用Python和Lean对这些方案进行验证，那么双方的方法很可能是相似的。

ZP：你怎么看通用前沿模型与专门做 AI for Math 的公司，两者各自的价值？

Axiom：前沿模型的能力正在越来越强，但运行成本也非常高。

ZP：参与这个项目的六名团队成员分别是什么背景？大家是如何分工的？

Axiom：我们的团队由数学家和工程师组成。

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

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

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

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

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

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

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

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

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