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

背景

在人工智能快速渗透科研领域的当下，数学这一高度依赖逻辑严密性的学科正迎来新的变革。近期，量子位报道了一则引发学界关注的消息：初创公司 Axiom Math 宣布，其系统生成的 8 篇数学论文中，已有 5 篇通过同行评审并被学术期刊接收。

这一突破的背后，是一位极具传奇色彩的 00 后创始人——洪乐潼。她出生于 2001 年，拥有 MIT 数学与物理双学位、罗德奖学金及摩根奖等顶尖荣誉，却在斯坦福大学攻读博士期间选择退学，全职投身于 AI 与数学交叉领域的创业。Axiom Math 在成立不到一年的时间内，完成了从种子轮到 A 轮的快速融资，估值达到 16 亿美元，显示出资本市场对“可验证 AI”这一方向的高度认可。

核心内容

Axiom Math 的核心产品是名为 AxiomProver 的 AI 系统。该系统并非简单地生成自然语言文本，而是致力于生成可被机器严格验证的形式化证明。

1. 论文成果与领域跨度 自 2026 年 2 月提交以来，Axiom Math 共提交了 8 篇论文，涵盖数论、组合数学、交换代数、代数几何、几何动力系统、表示论以及 Dyck path 模型等多个领域。截至 5 月 28 日，其中 5 篇已通过同行评审。

• 典型案例：论文《Reciprocals of Partition Polynomials》已被《Annals of Acad. Rom. Sci.》接收。该研究针对 Ballantine、Beck、Feigon 和 Maurischat 提出的 10 个猜想，AI 成功证明了其中 6 个，并发现了一个原始命题中的反例。
• 跨界尝试：5 月 27 日提交的最新论文涉及博弈论和经济学领域，与哈佛商学院教授 Scott Duke Kominers 合作，利用 Lean 语言形式化证明了 Robert Aumann 的经典定理。

2. 技术路径：人机协作新模式 AxiomProver 的工作流程解决了传统大模型在数学证明中存在的“逻辑缝隙”和“幻觉”问题：

• 输入：研究者提供自然语言的问题陈述。
• 核心处理：系统将问题翻译为 Lean 形式化证明语言。
• 验证：由单独的检测器对每一步推导进行机器验证，确保逻辑无懈可击。
• 输出：生成的形式化证明由人类数学家（如知名数学家 Ken Ono）配上学术解释，形成最终论文。

在这种模式下，AI 负责生成或形式化可检查的证明，而人类数学家负责问题表达、论文解释和审稿沟通。知名数学家 Ken Ono 指出，在某些开放研究问题上，系统能在约 24 小时内生成完整且经机器验证的证明。

3. 创始人背景与公司融资

• 洪乐潼：14 岁立志 MIT，17 岁考入 MIT，3 年拿下数学与物理双学位，本科发表 9 篇论文。后赴牛津大学攻读神经科学硕士，再获斯坦福数学与法学双博士学位录取。2024 年秋季因创业从斯坦福退学。
• 团队构成：联合创始人 Shubho Sengupta 前 Meta 员工；首席数学家 Ken Ono 辞去弗吉尼亚大学终身教职全职加入。
• 融资情况：3 月完成 2 亿美元（约 13.56 亿元人民币）A 轮融资，加上此前的 6400 万美元种子轮，总融资额达 2.64 亿美元，公司估值 16 亿美元。

关键要点

• 可验证性突破：AxiomProver 生成的不是仅具可读性的自然语言证明，而是基于 Lean 语言的形式化证明，每一步均可由机器验证，从根本上消除了 AI 幻觉带来的逻辑错误。
• 高效科研辅助：在给定开放研究问题的情况下，系统能在 24 小时内生成完整证明，极大提升了数学研究的效率。
• 顶尖人才汇聚：团队由 00 后天才创始人、前 Meta 工程师以及辞去终身教职的知名数学家 Ken Ono 组成，兼具技术实现能力与深厚的数学底蕴。
• 资本高度看好：不到一年时间融资超 2.6 亿美元，估值 16 亿美元，投资人 Matt Kraning 评价：“AI 将编写所有代码，但数学将证明其是否有效。”
• 能力验证：AxiomProver 曾在普特南数学竞赛中取得满分，并解决了两个困扰学界数十年的 Erdős 猜想。
• 未来愿景：Axiom Math 不仅限于数学，旨在打造能够自我改进的超级智能推理器，并将“生成、形式化、验证”的闭环应用至其他学科及高风险决策场景。

意义与影响

Axiom Math 的成功标志着 AI 在科学推理领域从“概率性生成”向“确定性验证”的关键转折。

首先，它解决了 AI 在严谨科学领域应用的信任危机。传统大模型虽然能写出流畅的自然语言证明，但难以保证逻辑的绝对严密。Axiom 通过引入形式化验证机制，证明了 AI 可以成为可靠的科研伙伴，而非仅仅是灵感激发器。

其次，这种“人机协作”模式为科研范式带来了新可能。人类负责提出高维度的问题和构建理论框架，AI 负责繁琐的逻辑推导和验证。这种分工不仅提高了研究效率，也可能加速基础科学的突破。

最后，其技术路径具有广泛的迁移潜力。既然 AI 能够处理高度抽象和逻辑严密的数学证明，那么同样的“生成-形式化-验证”闭环有望应用于软件工程、法律推理、医疗诊断等高风险决策领域。随着 Axiom Math 向博弈论、经济学等领域的拓展，我们正见证一个由可验证 AI 驱动的新科研时代的到来。