AI生成数学论文首被接收，00后创始人融资14亿

AI写的数学论文，已经能通过同行评审了？

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

事情是这样的：初创公司Axiom Math宣布，从2026年2月开始提交的8篇论文，到5月28日已有5篇通过同行评审，正式登上学术期刊。

创始人洪乐潼，2001年生于广州，本科三年在MIT拿下数学与物理双学位，还拿过北美数学本科生的最高荣誉——罗德奖学金和摩根奖。但在斯坦福读博期间，她退学了，理由就是创立Axiom Math。

Axiom在3月完成2亿美元（约13.56亿元软妹币）融资，估值16亿美元（约108.46亿元软妹币）。这批提交的论文横跨数论、组合、交换代数、代数几何/几何动力系统、表示论和Dyck path模型。

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

要理解Axiom Math到底在做什么，这8篇论文就是最好的切入点。

其中一篇叫Reciprocals of Partition Polynomials，已经被Annals of Acad. Rom. Sci.接收。这篇研究的是由partition subsum polynomials构造出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篇学术论文。毕业后赴牛津攻读神经科学硕士，再次接触了AI和机器学习研究。随后被斯坦福大学数学博士和法学博士双学位录取。但为了全身心创业，她于2024年秋季从斯坦福退学。

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

AxiomProver在普特南数学竞赛拿下满分，还解决了两个困扰学界数十年的Erdős猜想。但“AI数学家”只是Axiom Math的第一步，他们的愿景是打造一个能自我改进的超级智能推理器。

不到一年，Axiom完成了6400万美元种子轮和2亿美元A轮融资，估值飙到16亿美元。投资人Matt Kraning的评价直指核心：“AI将编写所有代码，但数学将证明其是否有效。”

如果一个AI系统能把数学证明交给机器逐步检查，那么同样的“生成、形式化、验证”闭环，也可能被拿去处理其他学科，以及高风险决策场景。5月27日，Axiom提交的最新一篇论文就跨界到了博弈论和经济学领域——与哈佛商学院教授Scott Duke Kominers合作，用Lean形式化证明Robert Aumann的经典定理。

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