由一支初创团队打造的“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人”榜单 图源福布斯官网 洪乐潼照片 受访者供图本文链接：24岁博士生退学创业，开发“AI数学家”连克难题http://www.sushuapos.com/show-11-29165-0.html
声明：本网站为非营利性网站，本网页内容由互联网博主自发贡献，不代表本站观点，本站不承担任何法律责任。天上不会到馅饼，请大家谨防诈骗！若有侵权等问题请及时与本网联系，我们将在第一时间删除处理。
上一篇： 第三届数字地球青年创新论坛在肯尼亚召开