数学论文预印本里，悄悄混进了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篇学术论文。
本科毕业后，她赴牛津大学攻读神经科学硕士学位，再次旗舰接触了人工智能和机器学习研究。
随后她被斯坦福大学的数学博士和法学博士双学位录取。
为了全身心投入创业，她于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年才能解决的那种。
现在看起来，她选的这条路同样也是最被关注的之一。
参考链接：
[1]https://x.com/axiommathai/status/2059640254341284320
[2]https://axiommath.ai/papers
本文来自微信公众号“量子位”，作者：梦晨，36氪经授权发布。
