数学学术界近日迎来了一场技术地震。初创AI公司Axiom Math对外宣布，其自主研发的AI系统自今年 2 月以来提交的 8 篇数学论文中，已有 5 篇正式通过同行评审并被学术期刊接收。这一突破不仅展示了人工智能在纯数学研究领域的巨大潜力，更标志着AI在解决高难度复杂学术猜想上迈出了实质性的一步。
在这批被接收的论文中，一项关于分拆多项式倒数和（Reciprocals of Partition Polynomials）的研究成果尤为引人瞩目。该研究直接瞄准了学界长期存在的 10 个核心猜想，AI系统不仅成功证明了其中的 6 个，甚至还敏锐地发现了原始命题中的一个反例。与以往只会用自然语言撰写“似是而非”证明的大模型不同，该团队研发的AxiomProver系统开创了全新的工作流：它能将自然语言表达的数学问题精确翻译为Lean形式化证明，并由独立的检测器对每一步逻辑进行严密验证。这种“机器证明、机器检查、人类数学家润色解释”的人机协作模式，从根本上杜绝了AI的“逻辑幻觉”。
而这一硬核科技成果的幕后推手，是一位年仅 25 岁的中国姑娘。Axiom Math的创始人洪乐潼 2001 年出生于广州，自幼便展露出惊人的数学天赋。她 17 岁考入麻省理工学院（MIT），仅用三年时间便斩获数学与物理双学位，并在本科期间发表了 9 篇论文。在相继拿下牛津大学硕士以及斯坦福大学法学与数学双博士录取资格后，她毅然决定于 2024 年秋季从斯坦福退学，全职投入创业。
洪乐潼的硬核背景和可验证AI的宏大愿景，吸引了顶级人才与资本的疯狂涌入。前Meta AI专家Shubho Sengupta以及知名数学家Ken Ono（小野健）相继加入成为其创业合伙人，后者甚至为此辞去了弗吉尼亚大学的终身教职。在不到一年的时间里，Axiom Math便完成了两轮共计2. 64 亿美元（约合 14 亿元人民币）的融资，公司估值直接飙升至 16 亿美元。
据了解，AxiomProver在此前就已经在普特南数学竞赛中拿下满分，并攻克了困扰学术界数十年的两个埃尔德什（Erdős）猜想。然而，洪乐潼和团队的野心远不止于“AI数学家”，他们的最新研究已经跨界至博弈论与经济学领域。该团队正致力于将这种“生成、形式化、验证”的闭环推理能力，推向其他高风险、高精度要求的决策场景，打造一个能够自我改进的超级智能推理器。
