【2026 Science x AI Summit 系列演讲切片第七期—Carina Hong】

在2026 Science x AI Summit上，Axiom创始人兼首席执行官Carina Hong指出，AI在数学奥林匹克中的表现已从突破走向常态，但真正的挑战在于：AI能否做出原创性的数学研究。

衡量数学研究进展缺乏可靠基准。Erdos问题曾因“AI找到十个未解答案”的新闻引发热议，实则多为文献检索而非原创证明。Axiom选择更硬核的路径：以Lean形式化语言为基底，构建混合式AI系统，输出可验证的数学证明。

自今年2月起，Axiom已发布7篇数学研究论文，其中5篇涉及形式化定理证明，涵盖数论、交换代数、代数几何等领域。代表性成果包括：关于“几乎所有素数都是部分正则的”定理，以及Ramanujan tau函数取素数分布密度为零的证明。两项成果均被数学期刊接收。

从解决Erdos问题（约50个推理节点）到证明Ramanujan tau函数性质（约500个推理节点），AI的推理能力正在快速跃升。Axiom的技术路线是混合式多智能体协作，并开源了“Axo”工具集以加速Lean形式化验证。

Carina Hong展望：AI for Mathematics正处于从“解题”迈向“发现”的转折点。数学发现不再是天才的专利，而将成为可验证、可扩展的智能协作过程。

这正是SAIR“验证优先”理念的前沿实践。

“数学发现的未来不取决于AI解题的速度，而取决于每一步推理能否被形式化验证所锚定。”——SAIR，与思考者同行。

#AI##AIforscience##SAIR##科研##AG##人工智能 ##AGI ##AI辅助数学##SAIRFoundation##数学##科学##验证##AI人工智能# http://t.cn/AXX0yotu