梦晨 发自 凹非寺量子位 | 公众号 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