务工家庭走出 00 后天才！退学造 110 亿独角兽，终身教授辞职追随

就在上周，全球创投圈被一个名字刷屏了。

AI 初创公司 Axiom 宣布完成 2 亿美元 A 轮融资，由硅谷顶级风投 Menlo Ventures 领投，Greycroft、Madrona Venture、B Capital、Toyota Ventures 等老股东全部跟投。公司估值飙升至 16 亿美元。

成立不到一年，直接跻身独角兽。但更让人震撼的，是这家公司的创始人 ——25 岁的洪乐潼（Carina Hong）。她让大模型的推理过程像数学证明一样严格，每一步都可验证。

洪乐潼祖籍潮汕，出生在广州，父母是普通务工者，但她从小就展现出极其罕见的数学天赋。

高一时，她入选广东省中学生英才计划，师从中山大学教授王学钦。随后，她在全国中学生数学奥林匹克（CMO）广东选拔中脱颖而出，成为仅有的四位女生之一。

2018 年，17 岁的洪乐潼被麻省理工学院（MIT）录取，选择了数学与物理双专业。

接下来的履历，堪称「开挂」。

她在 MIT 只用 3 年就修完两个学位，本科期间发表了 9 篇学术论文，研究方向涵盖模椭圆曲线、K3 曲面上的 L 函数、「月光猜想」等基础数学领域。

她曾获得全美女性数学家最高荣誉 ——Alice T. Schafer 数学奖，以及表彰北美数学专业本科生杰出研究的 AMS-MAA-SIAM 摩根奖。

2021 年，洪乐潼获得牛津大学罗德奖学金，成为当年仅有的四位中国获奖者之一。

罗德奖学金被誉为「本科诺贝尔奖」，是世界上历史最悠久、最负盛名的国际奖学金项目。

在牛津攻读神经科学硕士期间，她在伦敦大学学院盖茨比计算单位作为第一作者开展深度学习研究，正式踏入 AI 领域。

随后她又进入斯坦福大学，攻读数学与法律双学科博士。但博士还没读完，她就退学了。

洪乐潼看到的，是 AI 行业最尖锐的矛盾。大模型的能力在狂飙，但可靠性始终是个黑盒。

日常应用中的胡说八道或许无伤大雅，但在金融、国防、关键基础设施领域，任何基于概率的错误都可能酿成灾难。

去年针对 ChatGPT o3「数学测试作弊」争议，作为斯坦福数学博士的洪乐潼率先指出症结：当前 AI 缺乏严格的逻辑推理训练体系。

现有的大模型本质上是概率机器。它们通过海量数据学习模式，然后基于统计规律给出答案。即使是 GPT-4、Claude 这样的顶级模型，其概率性的本质依然是主要的担忧原因。

洪乐潼的答案是：让 AI 像数学家一样工作。

她创立的 Axiom 采用「数学即服务」模式，通过训练 AI 系统生成用 Lean 语言编写的、经过形式化验证的输出。

Lean 是一种专为数学证明设计的编程语言，通过使用 Lean，Axiom 可以确保 AI 模型推理过程的每一步都是可机器检查的并且在逻辑上得到保证。

传统大模型给你一个答案，你只能信或不信。而 Axiom 的系统给你一个答案，同时附带一个完整的、可验证的证明过程，不存在大概是对的这种模糊地带。

洪乐潼在接受采访时说：科学突破往往需要两步：提出假设，再用证明去验证。我们创立 Axiom，就是要无限压缩把好奇心转化为真理的时间。

去年 12 月，Axiom 交出了第一张成绩单。Axiom 的核心系统在普特南竞赛中，斩获满分，12 题全对。普特南竞赛是北美地区最负盛名的大学生数学竞赛，成绩的中位数常常为零（满分 120 分）。过去近百年，仅有 5 人达成过满分成就。Axiom 的 AI 做到了。

更震撼的还在后面。Axiom 可验证地证明了一个已有 20 年历史的数论猜想，该猜想涉及用于测量曲面距离的微积分元素。这个问题，连 Axiom 的创始数学家 Ken Ono 都曾多年尝试未能解决。

去年 12 月，Axiom 开发的 AxiomProver 系统，使用可验证的 Lean 语言，完成了埃尔德什问题集中第 124 题和第 481 题的形式化证明，分别用时 1 天和 5 小时，全程无人为干预。

埃尔德什问题集共包含 1109 个关于组合数学和数论的问题，是匈牙利数学家保罗 · 埃尔德什数十年来论文的汇集。

迄今为止，只有 266 个问题被证明，其中仅 10 个问题的证明被转化为计算机可验证的形式化版本。解决数学问题只是冰山一角。Axiom 正在将这种「绝对正确」的数学推理能力，通过迁移学习引入到代码验证领域，试图解决生成式 AI 的种种问题。

目标客户是对冲基金、量化交易员等高端场景。这些地方，容不得半点「大概对」。

Axiom 最震撼的一次招聘，发生在去年 12 月。Ken Ono（小野健），弗吉尼亚大学 Marvin Rosenblum 讲席教授、前美国数学学会副主席，辞去终身教职，全职加入 Axiom 担任创始数学家。

他是古根海姆奖、帕卡德奖、斯隆奖得主，世界顶尖的拉马努金数学权威之一，还是电影《知无涯者》的副制片人和数学顾问，甚至出演过百威啤酒的超级碗广告。

并且，他也是唯一一位出演过啤酒广告的数论学家。在 Ken Ono 长达四十年的执教生涯中，曾指导过十位摩根奖得主，洪乐潼正是其中之一。

为什么一个功成名就的终身教授，会放弃稳定的学术生涯，去为一个 25 岁的年轻人工作？华尔街日报报道称，Ken Ono 在人工智能彻底改变他的职业生涯和生活之前，一直对人工智能持怀疑态度。

直到最近，他开始谈论人工智能时，还总是嘲讽围绕这项新兴技术的炒作。但见到 Axiom 的系统后，他顿悟了。

除了 Ken Ono，Axiom 的团队堪称「梦之队」：CTO Shubho Sengupta 曾任 Meta AI 研究总监，此前参与过 Google 分布式训练系统的研究工作，也是最早开发 CUDA 技术的专家之一；核心科学家 François Charton，是率先将 Transformer 模型引入数学领域的先驱，曾用大模型推翻过一个长达 30 年未解的学术猜想。

一位投资人忍不住感慨：她兼具深厚的数学功底、惊人的运营效率，以及吸引世界一流人才的能力。这是我过去二十年的硅谷生涯中，见过的最令人印象深刻的创始人，没有之一。

目前，Axiom 拥有 30 多名员工，招聘速度还在不断加快。

就在上周，成立仅一年多的公司灵初智能宣布完成天使轮及 Pre-A 轮共计 20 亿元融资。其联合创始人陈源培，出生于 2001 年，曾就读于北京大学、斯坦福大学，师从李飞飞。

同为 00 后的杨丰瑜在耶鲁博士毕业后选择回国创业，2024 年成立了具身智能公司优理奇，完成数亿元的天使轮及天使 + 轮融资。

2025 年，由三位 00 后创立的 AI 招聘网站 Mercor 也宣布完成 1 亿美元的 B 轮融资，公司估值达 20 亿美元。

这一代创业者，和上一代有什么不同？

曾在 DeepSeek 火爆全球之际，洪乐潼发出这样的感慨：一个小而专注、特立独行的团队。一群理想主义者组成的优秀合作伙伴。他们执行力强，亲力亲为。最珍贵的，是那份理想与使命交织的信念。这就是 DeepSeek 的故事，也是我想亲自书写的故事。

有投资人私下交流时回忆，洪乐潼在创立 Axiom 期间于朋友圈写下的自勉：祝自己做花也做树。缤纷热情，孤离兀立。

谈话间，她几乎不谈论风口与颠覆，更多在意对问题本身的好奇和对技术可能性的清晰判断。

对于 Axiom 的终极使命，洪乐潼留下了一句极具张力的注脚：Verified AI 关注的，绝不仅仅是修补 AI 的缺点。真正瞄准的，是 AI 的上限，是通向超级智能的阶梯。

从广州普通家庭走出的女孩，到掌舵估值 110 亿的 AI 独角兽。从 MIT 的数学天才，到让终身教授辞职追随的创业者。洪乐潼和她这一代 00 后创业者的故事，正在改写硅谷的叙事规则：不是为了风口而创业，而是为了解决真正困难的技术问题。

AI 的上限在哪里？或许答案就藏在这群 25 岁年轻人的选择里。

参考资料：

https://mp.weixin.qq.com/s/msJXxZMSyfXMXDPMCdtznQ

本文来自微信公众号：新智元（ID：AI_era），作者：新智元