5篇AI生成的数学论文被接收，00后创始人洪乐潼融资14个亿

数学论文预印本里，悄悄混进了8篇AI作品。准确地说，是由同一套系统生成、完成形式化证明的8篇论文。

这事儿要从一家叫Axiom Math的初创公司说起。他们从2026年2月开始往学术期刊投稿，到5月28日，8篇中有5篇已经通过了同行评审，正式被期刊接收。

公司的创始人洪乐潼，2001年出生在广州。MIT本科三年拿下数学与物理双学位，还拿过北美数学本科生的最高荣誉——罗德奖学金和摩根奖。后来在斯坦福读博，她退学了。退学原因？正是创办Axiom Math。

这家公司在3月完成了一笔2亿美元（约13.56亿元软妹币）的融资，估值飙升到16亿美元（约108.46亿元软妹币）。这批提交的论文，横跨数论、组合数学、交换代数、代数几何与几何动力系统、表示论以及Dyck路径模型等多个领域。

AI证明，机器检查，人类审稿

要理解Axiom Math到底在做什么，这8篇论文就是最好的切入点。其中一篇关于Partition多项式倒数的论文，已经被《Annals of Acad. Rom. Sci.》接收。这篇论文的思路，是从所谓的partition subsum多项式出发，构造reciprocal sums，目标是攻克Ballantine、Beck、Feigon和Maurischat提出的10个猜想。最终，AI证明了其中6个，还在其中一个原始命题里发现了一个反例。

这个AI系统叫AxiomProver，它的厉害之处在于，产出不是停留在自然语言层面，而是直接生成形式化证明。现在的大模型当然能写出看起来很像模像样的证明文字，但问题在于，自然语言写成的证明，哪怕再顺滑，背后也可能藏着逻辑缝隙。读者、审稿人甚至作者本人，都得靠自己的理解和直觉去判断哪些地方站得住，哪些地方有漏洞。

AxiomProver换了一套交付方式：研究者给出自然语言的问题陈述，系统把这个问题翻译成Lean语言的形式化证明。翻译完成后，再有一个独立的检测器去验证每一个推理步骤是否合法。

论文的最终文本，仍然由人类数学家负责把形式化证明配上清晰易懂的学术解释。所以在这个实验里，AI并没有取代人类，而是实践了一种新的人机协作模式：AI负责生成或形式化可检查的证明，人类数学家负责问题表达、论文解释和与审稿人的沟通。

Axiom的创始数学家Ken Ono（小野健）表示，在某些情况下，系统被给定一个开放的研究问题后，大概在24小时内就能生成一个完整的、经过了机器验证的证明。

00后华人创办，布局可验证AI

回过头来看创始人洪乐潼的故事。她从小就在数学上展现出非凡的天赋，父母也给了很多支持。14岁的时候，她就在草稿纸上写下“MIT”来激励自己。高中就读于华南师范大学附属中学，进了广东省数学奥林匹克省队，在多项全国数学竞赛中拿过奖。

2019年，17岁的洪乐潼考入MIT。三年时间修完了数学和物理的双学位，本科期间就发表了9篇学术论文。毕业后，她又去了牛津大学读神经科学硕士，在那里首次接触了人工智能和机器学习研究。随后，她被斯坦福大学数学博士和法学博士的双学位项目录取。为了全身心投入创业，她在2024年秋季从斯坦福大学退学。

她的创业伙伴Shubho Sengupta也从Meta辞职。两人从AI与数学推理的交叉点入手，决心要解决AI的“幻觉”问题。后来，知名数学家Ken Ono甚至为此辞去了弗吉尼亚大学的终身教职，全职加入了团队。

AxiomProver在普特南数学竞赛里拿了满分，还解决了两个困扰学界几十年的Erdős猜想。“AI数学家”只是第一步，这家公司的愿景是打造一个能够自我改进的超级智能推理器。不到一年，Axiom就完成了6400万美元的种子轮和2亿美元的A轮融资，估值飙到了16亿美元。

投资人Matt Kraning的评价很有意思：“AI将编写所有代码，但数学将证明其是否有效。”如果一个AI系统能把数学证明交给机器逐步检查，那么同样的“生成、形式化、验证”闭环，理论上也能被移植到其他学科，以及那些高风险决策场景里去。5月27日，Axiom提交的最新一篇论文就跨到了博弈论和经济学领域，与哈佛商学院教授Scott Duke Kominers合作，用Lean形式化证明了Robert Aumann的经典定理。

洪乐潼曾经说过，创业者要选最难的问题，那种甚至需要5到10年才能解决的大难题。现在看起来，她选的这条路，同样也是最被关注的方向之一。

参考链接：

[1]https://x.com/axiommathai/status/2059640254341284320

[2]https://axiommath.ai/papers