656行代码5小时搞定，Axiom AI自主完成两项Erdős猜想形式化证明

近日，AI 初创公司 Axiom 宣布其模型在没有人类干预的情况下，自动完成了两个数学猜想的证明——埃尔德什问题（Erdős Problem）中的 481 号和 124 号。

据称，481 号问题仅用时 5 小时，代码量为 656 行；124 号问题则耗时超 24 小时。值得关注的是，这些证明均通过 Lean 验证，Lean 的特点是其形式化证明过程无需人工干预，为数学正确性提供了保障。

（来源：X）

据悉，本次完成两个数学猜想的证明的并不是 Axiom 推出的 API 或完整的产品，而是一个由多个模型组成的系统，包括 Axiom 的通过强化学习后训练研发的模型。

该公司 CEO 洪乐潼（Carina Hong）对 DeepTech 表示：“六百多行代码对于形式化的证明来说，算是比较简洁和漂亮的证明。”

（来源：X）

该证明在社交媒体发布后，有用户评价称“埃尔德什问题的精简形式化令人耳目一新”，也有用户评价本次证明是一个“好的起点”，还有用户这样评价：“几周前 OpenAI 曾称声称用 GPT-5 解决了埃尔德什问题，但社区指出它只检索了现有文献。而 Axiom 实际上证明了这个问题。”

图丨X 上用户评论（来源：X）

埃尔德什问题是匈牙利数学家保罗·埃尔德什（Paul Erdős）提出的一系列悬而未决的数学猜想，长期被视为检验推理能力的试金石。

图丨埃尔德什问题 481 号（来源：Erdős Problem）

481 号问题是一个社区近 45 年未被解决的问题，即某种迭代算术过程是否必然在某一步产生重复，从而进入循环或重复状态。

图丨Axiom 模型证明的 481 号问题（来源：洪乐潼）

而 124 号问题是：考虑若干整数基数 (d_1 < d_2 < \cdots < d_r)（且每个 (d_i \ge 3)），构造由这些基数的不同比例幂构成的序列。这是一个近 30 年未被解决的问题，也是最近比较火热的话题之一。

几天前，我们对 Harmonic 公司开发的 Aristotle 模型自主解决埃尔德什问题 124 号进行了报道，该公司由 Robinhood 的 CEO 弗拉德·特涅夫（Vlad Tenev）创立。

图丨埃尔德什问题 124 号（来源：Erdős Problem）

“关于 124 号问题，我们跑了超过一天的时间，中途一定是走到某个‘死胡同’里了。尽管目前跑出来的证明比较长，不如我们期望的简练，但至少它跑出来了。”洪乐潼说。

图丨Axiom 模型证明的 124 号问题（来源：洪乐潼）

Axiom 是一家成立不到 4 个月的公司，据公开资料其目前已融资 6,400 万美元的种子轮融资，成员不到 20 人。该公司 CEO 洪乐潼是 00 后，她在美国麻省理工学院获得数学和物理双学士学位，并在英国牛津大学获得神经科学硕士学位。此前，她曾在美国斯坦福大学攻读数学和法学博士学位，后辍学。

Axiom 官网称，其创新性体现在通过融合 AI、编程语言和数学，开发能够解决复杂数学问题的人工智能系统，其初始模型是 AI 数学家。一方面，其可启发人类数学家的科研灵感，另一方面可成为人类数学家的合作者，而非替代者。最新公开消息显示，著名数学家小野健（Ken Ono）刚从美国弗吉尼亚大学离职加入 Axiom 担任创始数学家，他曾在 2020 年担任洪乐潼研究项目的导师。

该公司官网提到，我们现在处于一个“数学发现”的时代。其在博客中曾提到过一个想法：人类在自然语言中进行推理，而该公司的模型在进行形式化推理时，会把自然语言的推理过程转化为形式化代码。在这个过程中，形式化代码的运行结果会反馈回来，进而影响人类在自然语言推理上的直觉和思考方式。

实际上，这个过程可以拓展到更广泛的应用领域，比如金融、量化交易、芯片、硬件和软件的形式验证、物理定律的形式化推导等。

自动形式化是近年来被关注新的方向，其把自然语言的证明转换到 Lean 语言中，这个过程与证明和形式化证明同样重要，且在一个系统中同时训练，而不是分开训练。

洪乐潼对 DeepTech 解释道：“我们对数据主要依赖自动生成，无论是从自然语言到形式化的自动转换，还是在形式化的基础上自动生成 100 到 1,000 倍的变体，甚至可以借鉴类似编译器中的想法和手段。”

据了解，Axiom 目前正在设计内部的基准数据集，旨在用更难的数据集来挑战其模型能否进一步突破极限。此外，他们还希望让猜想和证明可以做持续的非对称自我博弈以及事后重演。

洪乐潼认为，AI for Maths 是 AI for Science 的理论层和算法层，她表示：“大家可能觉得解决了埃尔德什问题很了不起，但我认为这只能说明模型具备了一定的能力，但我们也必须清醒地看到，它距离成为真正的 AI 数学家还有一定的距离，比如在数论、代数几何、代数拓扑、微分拓扑等方向上我们还有很大的进步空间。”

从融资规模与公司体量来看，Axiom 当前进展已引发行业关注。后续能否进一步与竞争对手拉开差距并形成落地产品，还需多一些的耐心与观察。

参考资料：

https://x.com/carinalhong/status/1995905801719066763?s=46

https://b.capital/why-we-invested/toward-mathematical-superintelligence-why-we-invested-in-axiom/

https://axiommath.ai/

https://www.erdosproblems.com/

https://techfundingnews.com/axiom-math-ai-mathematician-64m-seed/

https://www.wsj.com/tech/ai/math-ken-ono-carina-hong-axiom-startup-649bc417

运营/排版：何晨龙