AI初创公司Axiom实现数学猜想自动证明突破
近日，成立不足4个月的AI初创公司Axiom宣布，其自主研发的多模型系统在无人工干预下，成功完成埃尔德什问题（Erdős Problem）中第481号与第124号两个长期悬而未决数学猜想的形式化证明。
（来源：X）
481号问题：45年未解，5小时完成形式化证明
第481号问题是一个迭代算术过程是否必然进入循环的判定问题，社区持续探索近45年未果。Axiom系统仅用5小时、656行Lean代码即完成全部形式化证明，且经Lean验证器全程自动校验，确保数学正确性[2]。
（来源：X）
124号问题：30年难题，首获自动形式化证明
第124号问题涉及整数基数不同比例幂构成序列的结构性质，属近30年未解难题。Axiom系统耗时超24小时完成证明，虽当前版本代码较长，但首次实现该问题从自然语言陈述到Lean形式化证明的端到端自动转化[3]。
图丨X 上用户评论（来源：X）
图丨埃尔德什问题 481 号（来源：Erdős Problem）
图丨Axiom 模型证明的 481 号问题（来源：洪乐潼）
图丨埃尔德什问题 124 号（来源：Erdős Problem）
图丨Axiom 模型证明的 124 号问题（来源：洪乐潼）
Axiom技术路径与团队背景
Axiom并非依赖单一API或通用大模型，而是构建了融合强化学习训练模型、编程语言与数学推理的专用系统，核心目标是打造可协作的“AI数学家”[4]。其技术强调自然语言推理与Lean形式化代码的双向反馈闭环，支持自动数据生成、变体扩充及编译器启发式优化[5]。
公司CEO洪乐潼为00后，拥有麻省理工学院数学与物理双学士、牛津大学神经科学硕士学位，曾于斯坦福大学攻读数学与法学博士（后辍学）[6]。目前团队规模不足20人，已获6400万美元种子轮融资。著名数论学家小野健（Ken Ono）近期加入担任创始数学家，曾于2020年指导洪乐潼相关研究[7]。
行业意义与后续方向
埃尔德什问题被公认为检验AI推理能力的试金石。此次突破标志着自动形式化（Autoformalization）——即自然语言证明向Lean等证明助手语言的自动转化——正从理论走向实践验证阶段[8]。Axiom正构建高难度内部基准数据集，推动模型开展非对称自我博弈与事后重演训练[9]。
洪乐潼指出：“解决埃尔德什问题体现的是模型基础能力，但距离真正胜任数论、代数几何等前沿领域仍有显著差距。AI for Maths，本质是AI for Science的理论与算法基石。”[10]