💡 站外导读：当AI大模型还在为生成“幻觉”和逻辑谬误而困扰时，一家由00后华人少女创立的初创公司，已悄然实现了AI在纯数学领域的重大突破。Axiom Math不仅用AI证明了多个长期未决的数学猜想，更开创了“机器证明、机器检查”的可验证工作流，从根本上解决了AI推理的可靠性问题。这背后，是创始人洪乐潼从MIT到斯坦福的顶尖学术背景，以及对AI推理能力极限的挑战。在资本与顶尖人才的加持下，这项技术正从数学象牙塔，走向博弈论、经济学等更广阔的决策场景，预示着一个能够自我改进的超级智能推理器时代的到来。
数学学术界近日迎来了一场技术地震。初创AI公司Axiom Math对外宣布，其自主研发的AI系统自今年 2 月以来提交的 8 篇数学论文中，已有 5 篇正式通过同行评审并被学术期刊接收。这一突破不仅展示了人工智能在纯数学研究领域的巨大潜力，更标志着AI在解决高难度复杂学术猜想上迈出了实质性的一步。
在收到的这批论文里，一篇关于“分拆多项式倒数和”的研究格外亮眼。它直接向数学界长期悬而未决的十大核心猜想发起挑战，其背后的AI系统不仅成功证明了其中六个，还敏锐地找到了原始命题中的一个反例。与那些只会用自然语言生成“看似合理”证明的大模型截然不同，这支团队打造的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数学家”，他们的最新研究已经跨界至博弈论与经济学领域。该团队正致力于将这种“生成、形式化、验证”的闭环推理能力，推向其他高风险、高精度要求的决策场景，打造一个能够自我改进的超级智能推理器。
📝 站长洞察 (Editor’s Insight)
Axiom Math的突破，其意义远超几篇被接收的论文。它揭示了一个关键范式转移：AI的进化正从“概率生成”迈向“逻辑验证”。传统大模型本质是“语义拟合”，而AxiomProver通过将问题形式化，并引入独立验证器，构建了一个逻辑闭环，这为解决AI的可信度与可靠性这一核心产业痛点提供了可行路径。洪乐潼的路径极具代表性——顶尖学术青年将前沿理论与工程能力结合，切入最高智力密度的数学领域作为“技术验证场”，再向金融、科研等高价值决策场景辐射。这不仅是技术的胜利，更是“AI for Science”向“AI as Scientist”演进的里程碑。当AI能自主进行高难度创造性推理时，它将不再仅是工具，而是具备认知增强能力的合作伙伴，其颠覆的将是知识生产的底层逻辑。资本疯狂押注的，正是这种重塑科学与决策流程的通用推理引擎潜力。
