当57岁“数学传奇”决定为24岁“天才少女”的AI项目打工

数学家小野健（Ken Ono）和他的学生洪乐潼，图片来源：WSJ

最近，美国一位传奇数学家，放下了终身教职，开始为一位24岁的年轻人“打工”。

据《华尔街日报》，57岁的美国顶尖数学家小野健（Ken Ono）辞去了弗吉尼亚大学终身教职，上周正式加入了他之前的学生，一位24岁年轻人洪乐潼（Carina Hong）创办的AI数学公司Axiom Math，成为第15号员工。

小野健出生于1968年，是美国顶尖数论学家，弗吉尼亚大学终身教授，研究领域为数论（ number theory），曾任弗吉尼亚大学教务长STEM顾问。

当然，洪乐潼亦是一位数学界的“天才少女”。她用三年时间从麻省理工学院毕业，作为美国顶尖的本科数学研究者荣获摩根奖（Morgan Prize），并获得罗德奖学金（Rhodes scholarship）。

之后，她前往斯坦福大学攻读法律和数学双博士学位。中途，她决定退学创办Axiom Math，并完成了6400万美元的融资，从Meta挖来数名AI研究员，以及，请来了她的导师。

小野健的决定，在数学界与AI圈都引起广泛关注，因为这是少有的顶尖纯数学家转身投入AI创业公司的案例，也意味着“数学研究+AI”有了一种新方向。

24岁的“天才少女”与震惊AI圈的Axiom Math

两年前，22岁的洪乐潼在硅谷创办了Axiom Math，目标是打造“AI数学家”：一种AI系统能够像人类数学家那样推理、发现、并证明数学定理。

Axiom Math成立后不久便完成了6400万美元的种子轮融资，由B Capital领投，Greycroft，Madrona Venture Group和Menlo Ventures参投，融资后公司估值达到3亿美元。

在Axiom Math官网，有一则颇令人心潮澎湃的使命宣言：

数学发现使我们能够理解从人脑到宇宙的每一个复杂系统。纵观人类历史，每一种数学工具都极大地扩展和加快了后续发现的规模和速度。 人工智能正处于一个历史性的转折点：数学发现可以以指数级规模和令人振奋的速度展开。我们正站在数学复兴的门槛上。 这场复兴建立在三大支柱之上：人工智能、编程语言和数学。数学家与人工智能的合作，以前所未有的规模和速度创造出新的想法。编程语言将抽象概念转化为可验证的现实。它们共同创造了一个发现的飞轮：每一次突破都加速着下一次的到来。 我们正在组建一支首次在所有三个领域都拥有精湛技艺的团队。他们是利用人工智能打破曾经难以逾越的障碍的先驱者：大规模同步训练的架构师、将人工智能引入代码生成的远见卓识者，以及运用Transformer解决百年数学猜想的开拓者。 数学发现的未来从这里开始。

洪乐潼本人一直对数学发现抱有极大兴趣。她发现，奥数带来的是持续的多巴胺刺激，而研究型数学更像是“拿头撞墙”的过程，这是一种痛苦与磨砺，而她正喜欢这点。

Axiom Math的研究方向，包括大模型形式化定理证明、合成数学数据生成、猜想自动提出与验证，以及面向芯片设计、物流优化、金融系统的高阶算法自动发现。

创业仅4个月，洪乐潼带领不足10人的团队（核心成员仅4人），用自主研发的Axiom Prover系统，可在分钟级完成IMO银牌难度几何题，并接连攻克两道悬而未决的数学难题，震惊数学界与AI圈：

• 埃尔德什第124题（加法数论问题，悬置30年）：全程无人干预，1天内完成基础公理层面的形式化证明，远超竞品的简化版证明，成为全球首个可严格验证的解决方案。
• 埃尔德什第481题（迭代算术问题，悬置45年）：直接推翻OpenAI“GPT-5已解决”的不实声明，5小时内完成完整证明与形式化验证，证明过程被美国数学学会评价为“逻辑严谨、无任何隐性错误”。

这两项突破的核心优势的是“形式化验证”——通过Lean编程语言将数学证明转化为可执行程序，确保结果100%可信，而这正是洪乐潼结合数学研究与AI技术的创新之处，也让Axiom快速拉开与巨头的差距。

公司对外宣称不以“替代数学家”为终点，而是构建“人机共写”的新一代数学基础设施：让模型负责穷举与形式化，数学家负责直觉与价值判断，从而把平均发现周期缩短一个数量级。

Axiom Math的商业路线采取“底层模型+垂直SaaS”双轮模式，前期主要加速开发 “AI数学家”，针对benchmark 问题 (数学、算法、物理、加密) 测试与优化。

引擎成熟后，会推出给企业和机构的SaaS/API产品，主攻量化金融、风险管理、芯片/硬件验证、科研/R&D流程等领域。

AI让顶尖学者有了“身份危机”

小野健在Axiom Math的日常工作包括：给AI模型设计必须通过的数学难题，构建数学能力的基准测试，推动模型向“数学创造力”进化等。

作为数学巨人的另一面，小野健是极度“摇滚”，是“老顽童”。

2007年，《纽约时报》曾发表了一篇人物特写The Man Who Makes Math Rock（《这个让数学摇滚的人》），描述小野健在讲台上“像吉他手一样来回奔跑、用幻灯机打出爆炸式彩色公式”，并把他的演讲比作“数学演唱会”。后来，他还上过好莱坞啤酒广告，被ESPN称为“最会弹吉他的数学家”。

这种特立独行的行事风格，也难怪小野健从顶尖学府离职，加入年轻学生创办的新公司。

事实上，AI对于数学的影响远早于大众对于AI的理解。

1956年出现的“第一个人工智能程序”——Logic Theorist，证明了数学家阿弗烈·诺斯·怀特海（Alfred North Whitehead）和伯特兰·罗素（Bertrand Russell）的《数学原理》（Principia Mathematica）第二章中前52个定理中的38个，并为其中一些定理找到了新的、更简洁的证明。

2024年，DeepMind与纽约大学推出了一套名为Alpha Geometry的AI系统。该系统通过合成了约1亿条几何定理与证明作为训练数据，从零开始训练，没有人类示范。它在一个包含30道IMO-style几何题的测试集中，解出了25道。这个成绩非常接近过去人类IMO金牌选手在这些题目上的平均水平，被视为AI在复杂逻辑推理与数学证明方面的重要里程碑。

如果说1956年AI仅能证明人类已验证的理论，那么，到了2025年，AI已经可以接过教授的笔，并告诉他，“这个问题其实没那么难”。

AI数学已经在自主质疑和验证人类顶级数学家数百年来建立的学术成果，也难怪数学巨人也会对自己的身份认同产生动摇。

而小野健就曾一度对外这样自我介绍，“我是NI，天生智能（Naturally intelligent）”。

与AI与数学的历史刻度同步变得紧凑的，还有近年来全球顶尖科学家“弃研从创”的密度。

今年，美国国家工程院院士、美国国家医学院院士、美国艺术与科学院院士，美国斯坦福大学主要红杉讲授教授李飞飞创办了World Labs，专注世界模型（World Model）。

最近，AI教父级人物、图灵奖得主杨立昆（Yann LeCun）离职Meta，将创办一家专注于先进机器智能研究项目（AMI）的初创公司。

在中国也出现类似潮流。2016年，香港科技大学自动化技术中心主任李泽湘教授离开教研一线，全力孵化创新生态，成功投资孵化了大疆创新、云鲸智能等硬科技企业。

同样，在2016年，中国科学技术大学少年班数学与应用数学专业、中国科学技术大学计算机学院攻读博士陈天石，带领团队创立寒武纪，2025年，寒武纪以6643亿市值登顶A股“股王”。

事实上，教授跳槽进创业公司，并不是AI时代才有的新鲜事，自20世纪60年代硅谷形成“科技-资本-高校”三角生态以来，几乎每一次技术范式的更替，象牙塔里最稀缺的“大脑”都会被新兴产业“吸走”。

资本需要学术权威背书，而高校随即以“停薪留职、专利分成、创业休学”等制度降低机会成本，让教授跳槽成为“进可攻、退可守”的抉择。对高校来说，顶尖学者涌向产业，最直接的影响却是学校研究能力的断档。

科学家创业迁徙潮的另一面，会直接导致高校顶会论文的出稿率下滑，同步拉低基础科研经费，还会导致与关键学者有关的交叉学科萎缩。

不过，走出校园的顶尖“大脑”也并未切断与母校的联系，大多数成功的顶级学者都会以捐赠、兼职、公开课持续回流。

每一次顶级学者的人才外溢，都伴随着学科话语权大迁移。在学术圈常有人说，半导体看斯坦福与伯克利的电机系，生物医药看UCSF与哈佛医学院，互联网看斯坦福与卡内基梅隆的CS。而当今的AI，则是由卡内基梅隆大学（CMU）引领，与麻省理工、斯坦福、伯克利等顶尖院校共同驱动的格局。

在这前沿技术潮起潮落之间，那些未能及时做出反应的院系或者人才，命运也会随之起起落落。（作者｜陶天宇，编辑｜李程程）