由一支初创团队打造的“AI数学家”，接连攻克了两道几十年悬而未决的数学难题，并给出细化到基础公理的、可验证的证明。

12月3日，记者从初创公司Axiom Math联合创始人洪乐潼（Carina Hong）处获悉，该公司开发的AxiomProver系统，使用可验证的Lean语言，完成了埃尔德什问题集（Erd?s Problems）中第124题和第481题的形式化证明，分别用时1天和5小时，全程无人为干预。

该成果是Axiom Math打造AI数学家愿景的标志性进展，将AI大模型解决复杂问题的能力向前推进了一步。

埃尔德什问题集共包含1109个关于组合数学和数论的问题，是匈牙利数学家保罗·埃尔德什（Paul Erd?s）数十年来论文的汇集。迄今为止，只有266个问题被证明，只有10个问题的证明被转化为计算机可验证的形式化版本（Lean语言）。

其中，第124题是一个关于加法数论的问题，它探讨如何将整数表示为多个进制的幂之和。这个问题悬置了约30年。

第481题则询问某个迭代的算术过程是否必然最终产生重复元素。埃尔德什本人曾表示，它的难度之大“令人惊讶”。这个问题悬置了45年。

值得关注的是，此次突破由一支成立仅4个月、不足10人的小团队完成。

“我们一度不被看好。”洪乐潼坦言，相比于部分知名实验室，Axiom Math晚了两年进入市场，且在融资额和估值上仅有竞争对手的五分之一。

据悉，洪乐潼曾是斯坦福大学博士生，目前退学创业。她本科毕业于麻省理工学院，获数学和物理双学位，后在牛津大学获得神经科学硕士学位。她还曾获得表彰北美地区数学专业本科生杰出研究的AMS-MAA-SIAM摩根奖。就在12月3日，洪乐潼入选“福布斯30岁以下30人”榜单。

洪乐潼入选“福布斯30岁以下30人”榜单 图源福布斯官网

洪乐潼照片 受访者供图