8篇AI数学论文5篇被接收，00后华人洪乐潼创办Axiom Math，融资14亿
初创公司Axiom Math的AI系统AxiomProver在2026年2月至5月间提交了8篇数学论文，其中5篇已通过同行评审并被期刊接收。创始人洪乐潼为2001年出生的华人，MIT双学位退学创业，公司已完成2亿美元融资。系统采用生成形式化证明并用Lean验证的方式，确保证明无逻辑漏洞，目前已解决多个Erdős猜想并跨界应用到博弈论。
事件概述
2026年2月至5月，AI初创公司Axiom Math通过其系统AxiomProver提交了8篇数学论文，其中5篇已通过同行评审并被学术期刊接收。论文涵盖数论、组合学、交换代数、代数几何/几何动力系统、表示论和Dyck path模型等领域。
核心技术：AxiomProver
AxiomProver并非用自然语言生成证明，而是将问题转化为Lean形式化证明，再由独立检测器逐步骤验证。人类数学家负责将形式化证明配上学术解释，形成可发表的论文。这种模式杜绝了自然语言证明中可能隐藏的逻辑漏洞。联合创始人Ken Ono表示，系统在收到开放研究问题后，约24小时内即可生成完整、机器验证的证明。
代表性成果
一篇关于Partition Polynomials倒数的论文已被Annals of Acad. Rom. Sci.接收，AI证明了6个相关猜想并发现了一个原始命题中的反例。此外，系统曾在普特南数学竞赛中取得满分，并解决了两个Erdős猜想。2026年5月27日，最新论文跨界至博弈论与经济学，与哈佛商学院教授合作，用Lean形式化证明了Robert Aumann的经典定理。
创始人与融资
创始人洪乐潼（2001年生于广州），MIT三年完成数学与物理双学位，获罗德奖学金和摩根奖，在斯坦福攻读博士期间退学创业。联合创始人Shubho Sengupta从Meta辞职，数学家Ken Ono辞去弗吉尼亚大学终身教职加入。公司不到一年完成6400万美元种子轮和2亿美元A轮融资，估值16亿美元。投资人评价：“AI将编写所有代码，但数学将证明其是否有效。”
愿景
Axiom Math的目标是打造能自我改进的超级智能推理器。通过“生成-形式化-验证”闭环，该方法有望从数学扩展到其他学科和风险决策场景。