5篇AI生成的数学论文被接收！00后创始人洪乐潼融资14个亿
TL;DR · AI 摘要
Axiom Math的AI系统AxiomProver生成并形式化证明的8篇数学论文中，5篇已通过同行评审发表；其核心是“自然语言问题→Lean形式化→机器验证”闭环，00后创始人洪乐潼带队完成14亿人民币融资，估值达16亿美元。
核心要点
- AxiomProver在24小时内可生成完整、机器验证的数学证明，已解决6个Ballantine等提出的猜想并发现1个反例
- 公司3个月内完成6400万美元种子轮+2亿美元A轮（约14亿人民币），估值16亿美元，获Ken Ono等顶尖数学家全职加入
- 论文覆盖数论、代数几何、表示论等6大领域，最新一篇与哈佛商学院合作，用Lean形式化证明Aumann博弈论定理
结构提纲
按章节快速跳转。
Axiom Math自2026年2月提交8篇AI生成/形式化证明论文，截至5月28日已有5篇被学术期刊正式接收。
系统将自然语言问题翻译为Lean代码生成形式化证明，并由独立检测器逐行验证，确保逻辑无漏洞。
00后洪乐潼MIT三年双学位毕业，退学创业；Axiom完成2亿美元A轮融资，估值16亿美元，Ken Ono辞去教职全职加入。
最新论文跨界至经济学，与哈佛教授合作形式化证明Aumann定理，验证该框架可迁移至其他学科与关键决策场景。
AI负责生成与形式化证明，人类数学家主导问题定义、解释撰写与审稿沟通，形成互补型科研工作流。
思维导图
用一张图看清主题之间的关系。
查看大纲文本（无障碍 / 无 JS 友好）
- Axiom Math：AI驱动的可验证数学研究
- 技术核心
- AxiomProver系统
- 自然语言→Lean形式化→机器验证闭环
- 依赖Lean证明助手
- 成果与影响
- 8篇论文提交，5篇已发表
- 解决Erdős猜想×2、Ballantine等6个猜想
- 跨界至博弈论（Aumann定理）
- 团队与融资
- 洪乐潼（00后，MIT双学位，斯坦福退学）
- Ken Ono（全职加入，前弗吉尼亚大学教授）
- 2亿美元A轮 + 6400万种子轮，估值16亿
- 方法论创新
- 人机协作：AI证，人释/审
- 目标：构建自我改进的超级智能推理器
金句 / Highlights
值得收藏与分享的关键句。
AxiomProver在24小时内生成完整、机器验证的证明；在Reciprocals of Partition Polynomials一文中，AI证明了6个猜想并发现原始命题中的反例。
8篇提交论文横跨数论、组合、交换代数、代数几何/几何动力系统、表示论和Dyck path模型，体现系统广谱推理能力。
投资人Matt Kraning评价：‘AI将编写所有代码，但数学将证明其是否有效’，点明可验证AI对高可靠性系统的战略价值。
最新论文与哈佛商学院Scott Duke Kominers合作，用Lean形式化证明Robert Aumann经典博弈论定理，标志技术向交叉学科延伸。
< img id="wx_img" src="https://www.qbitai.com/wp-content/uploads/imgs/qbitai-logo-1.png" width="400" height="400">
2026-05-28 16:11:40 来源：量子位
8篇由同一个系统生成或形式化证明的数学论文
梦晨 发自 凹非寺
量子位 | 公众号 QbitAI
数学论文预印本里，悄悄混进了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
_版权所有，未经授权不得以任何形式转载及使用，违者必究。_