25 岁的洪乐潼，最近在硅谷火了。

这个来自广东的女孩，17 岁考入 MIT，三年修完数学和物理双学位，后来又进入斯坦福深造。

按照硅谷最熟悉的那套叙事，她是 " 天才少女创业者 " 的模板人物。

但洪乐潼真正让人记住的，不是履历，而是她做的事太反常识。

当整个 AI 行业都在追逐更大的模型、更强的生成能力、更像人的表达时，她偏偏转身去做了一件最不性感、也最难商业化的事：用数学验证 AI。

她创办的公司叫 Axiom，成立不足两年，员工只有 20 多人，最近拿下 2 亿美元 A 轮融资，投后估值高达 16 亿美元，折合人民币超 110 亿元。

Axiom 不做聊天机器人，不做文生图，也不跟风大语言模型的热潮。它做的是 " 形式化验证 "。

说白了，就是想用数学和逻辑，把 AI 每一步推理都变成可以检查、可以证明、可以追责的东西。

这听起来很冷门，但它瞄准的，却是大模型最麻烦的软肋——幻觉。

现在的 AI 最大的问题不是不够强，而是不够可靠。它可以把答案说得很像对的，甚至真的做对题，但你没法确认它到底是真的推出来了，还是只是 " 猜对了 "。而 Axiom 要做的，就是把这种模糊状态，变成一种可验证的确定性过程。

这也是为什么，当洪乐潼拿着这个想法去融资时，迎面撞上的不是掌声，而是一个极其现实的问题：" 数学怎么赚钱？"

01 迎难而上的天才少女

洪乐潼的办公室在硅谷帕洛阿尔托大学大道，距离斯坦福大学步行只要半个小时。斯坦福是她博士生涯的起点，但学位还没有念完，她就退学创业了。

事实上，早在博士在读期间，洪乐潼就已经注册了公司。公司取名 Axiom，名字源自数学术语 " 公里 "，" 我想从公理出发，打造一个能够自我改进的超级智能推理器。"

一个 24 岁的博士生，没钱没人没产品，仅凭一个想法，她就拿下了 960 万美元的种子轮投资。

凭什么？

要知道现有的大模型本质上是概率黑盒，通过海量数据学习模式，然后基于统计规律给出答案。推理过程无法被量化，所以会胡说、会出错。

洪乐潼要做的就是用数学公理和形式化验证，让 AI 每一步推理都可证明，可以直接面向金融、军工、芯片和自动驾驶等对可靠性要求极高的市场。

她做的事显然击中了 AI 最大痛点，解决幻觉与可靠性的问题。

更何况，早期投资投人，她本人也是不折不扣的跨学科天才学霸。

洪乐潼从小就展现出了惊人的数学天赋。2001 年，她出生于广州市天河区，曾就读于华南师大附中。高一时，她就在全国数学奥林匹克选拔赛中晋级，并在华罗庚杯、全国高中数学联赛中屡获佳绩。

正是在奥数集训中，她对研究型数学产生了兴趣。

2018 年，17 岁的她被 MIT 录取，3 年就修完了数学和物理双学位，不仅发表了 9 篇学术论文，还获得全美女性数学家最高荣誉 Alice T. Schafer 数学奖等诸多荣誉。

此后，她获得牛津大学罗德奖学金，她没有继续深耕数学，转头去学了神经科学，因为想 " 构建跨越科学领域的认知体系 "。

基于这一目标，她同时在伦敦大学学院盖茨比计算神经科学中心开展深度学习研究，该中心由 " 深度学习之父 " 杰弗里 · 辛顿联合创立。也正是在此期间，她正式踏足 AI 领域，接触到许多最前沿的课题。随后她又进入斯坦福大学，攻读数学与法律双学科博士。

2024 年，ChatGPT o3 被曝光在数学测试中存在 " 作弊 " 嫌疑，全球舆论哗然。

作为斯坦福数学博士的洪乐潼也在社交媒体上发表了看法："OpenAI 大模型在数学测试中表现优秀，大概率是因为训练数据中提前泄题了。在一些测试中，大模型回答的准确率虽然高达 96%，但一旦展示推理过程，得分率就降至 5%。"

面对行业痛点，一种名为 Lean 的语言闯入她的视线，也让她嗅到了创业机会。

与自然语言不同，Lean 语言是一个非常神奇的、可以自验证的数学编程语言。洪乐潼打了个比方：" 如果用英语写出数学证明，我没办法知道一个 5000 行的证明是否正确，需要找高水平的专家验证。但 Lean 是自验证的，只要跑通了就是对的。"

Lean 的逻辑是把自然语言或非形式化验证，转成机器可检查的形式化验证。

那啥是形式化验证呢？

普通的 AI，你只能用它的答案来判断它是不是理解这个问题，但你不知道它中间有没有瞎蒙。

形式化验证是要求你把每一步都写成机器能检查的逻辑链条。只要中间有一步跳了、糊了、偷懒了，它就不给过。

之所以形式化验证能治大模型会幻觉，是因为形式化验证不管你答案如何，只要你的结论是从前提里一步步合法推出来的，那答案就是对的，从而避免了模型产生幻觉。

所以 Axiom 做的，就是让大模型负责猜想和搜索，让 Lean 负责验算和判断。如果 Lean 检查发现过程不对，那就退回去继续改。

但这显然是一条窄路。这条路冷门到什么程度？在整个 AI 版图里，形式化验证几乎是边缘中的边缘，全球的商业化玩家一只手就数得过来。

显然她并不是因为形式化验证是下一个风口才选的，而是因为她对 " 困难 " 的定义和别人不一样。

奥赛就像持续释放多巴胺的快感，而研究型数学像在撞墙，充满痛苦与煎熬。我其实特别喜欢这种挑战感。" 她曾这样解释自己痴迷数学的原因。

正是这种刻在骨子里的挑战欲，让她不愿再停留在学术研究的舒适区，渴望在更广阔的战场上去攻克 AI 领域的硬骨头。

2024 年深秋，斯坦福附近的一家咖啡馆里，洪乐潼与当时 Meta AI 研究总监 Shubho Sengupta 聊了整整几个小时，核心议题只有一个：AI 能不能真正学会数学推理？

两人一拍即合，一个退学，一个辞职，两人一起创业。

02 一支 " 草根 " 工程师军团

Axiom 只有 20 多名员工，洪乐潼用了一个词来形容团队的气质：草根工程师精神。

但事实上，这支团队的成员身份一点也不草根，甚至背景堪称豪华。

Axiom 第一位成员，正是和她在咖啡馆聊了好几个小时的 Meta 前员工 Shubho Sengupta，如今他的身份是公司的 CTO。

核心科学家 François Charton，则是将 Transformer 架构引入数学推理领域的先驱人物。他干的活，就是把数学算式当成一种 " 语言 " 输入进 Transformer，试试看 Transformer 能不能像翻译句子一样去翻译数学。

其他成员约半数来自 Meta AI，另一半则是世界级数学家与形式化验证先驱。

而最让外界震惊的一位成员，是 57 岁的数学泰斗小野健（Ken Ono）。

他是模形式领域的顶尖学者，美国数学学会前副会长，拿过古根海姆奖、斯隆奖等荣誉。指导过的学生中有十位摩根奖得主。他还曾为美国奥运游泳队提供数据分析，为电影《知无涯者》担任顾问。

这位弗吉尼亚大学终身教授与洪乐潼结缘于麻省理工。彼时大一新生洪乐潼参与了他的数论项目。师生关系延续至今，角色却已不同，2025 年底，小野健辞去教职，全职加入 Axiom，成为第 15 号员工。

曾拒绝过 Google 和 Meta 邀请的小野健，为什么愿意为一个 24 岁的学生 " 打工 "？

" 如果我的猜想能被机器在 3 天内推广到 10 个维度，我愿意当一个‘标注工’。" 小野健曾公开表示，他选择帮自己的学生打工，不仅因为洪乐潼开出 " 不设教学、不设行政、100% 科研 " 的合约，更关键的是，AI 对他的 " 降维打击 "，让他感到兴奋。

一群顶级学者和前 Meta 成员，这个团队哪里草根了？

洪乐潼的解释是，草根，代表着始终 " 空杯 " 的心态和坚韧的品质。在创业这条路上，即使是资深 " 牛人 "，也要从头学起，不断自我革新。

她自己最喜欢的不是当 " 精英 "，而是做 " 草根 "，做个 nobody（小人物），这样学习的坡度最陡、速度最快。

她自己也是 " 草根精神 " 的践行者，在被问到如何带领团队时，洪乐潼说：" 我其实不太喜欢用带领这个词。我希望自己是一个 Individual contributor（独立贡献者），每个人都是，这是一群志同道合的人在一起做事。"

" 我们创立 Axiom，就是要无限压缩把好奇心转化为真理的时间 "，在资本驱动的硅谷，洪乐潼的这种纯粹性，对于顶尖研究者而言，或许比一份高薪 offer 更有吸引力。

这支不到 20 人的团队，在成立后不到一年就交出了一份令人意外的答卷。

2025 年 12 月 3 日，Axiom 宣布其核心系统 AxiomProver 在无人干预的情况下，攻克了困扰数学界数十年的两道埃尔德什难题。

同一天，洪乐潼收到了入选 " 福布斯 30 岁以下 30 人 " 榜单的消息。

同月，AxiomProver 又在普特南数学竞赛中斩获满分，12 道题全对。普特南是北美最负盛名的大学生数学竞赛，成绩的中位数常常为零，过去近百年仅有 5 个人类选手拿到过满分。

Axiom 进一步印证了用形式化验证构建可靠、可核验、无幻觉的 AI，已是行业明确的重要方向，而 AxiomProver 则在这条路径上交出了可复现、高难度的实证。

03 赛道升温，但挑战刚刚开始

从行业发展来看，洪乐潼的选择正好踩在了技术转折点上。

2024 年年底，Meta FAIR 和斯坦福大学等多所机构联合发布了一篇立场论文《Formal Mathematical Reasoning: A New Frontier in AI》。

论文给出了这样一个判断，过去的 AI 数学就是喂很多数学题，再让模型输出答案。这就导致数据会污染、过程会胡编，AI 没办法自判断对错，并且还很难复现过程。

这显然是路走错了。就拿乘法口诀表来说，里面写的是 2*3 得 6，那么你自己也能理解 3*2 就也得 6。这个过程就叫复现。

论文主张的是下一步要把证明助手、形式系统、自动验证真正接进模型里来，让 AI 真正懂数学。

但这也意味着这条窄路正在变得拥挤。

过去十年，AI 赛道的主流叙事是 " 更大参数、更多数据、更快生成 "，所有大公司都在这条路上狂奔。洪乐潼选择的形式化验证是其中冷门到几乎没有竞争的赛道。

今年年初，Meta 也发布了半形式化推理技术，让大语言模型能够在不执行代码的情况下验证代码补丁，准确率高达 93%。竞品公司 Harmonic 在今年 1 月获得了英伟达投资，估值达 14.5 亿美元，产品已扩展到代码编写和芯片设计领域。Theorem、Axiomatic AI、Cajal 等一批初创公司，也在近两年纷纷进入这个赛道。

对 Axiom 而言，挑战远不止行业竞争。

最大的挑战在于商业模式。洪乐潼最初的设想是将产品服务于对冲基金和量化交易公司，快速解决与资产定价、股市预测相关的复杂数学问题。

但这个蓝图至今仍停留在构想阶段。对高频交易而言，比 " 正确 " 更重要的是 " 足够快 "，毫秒级的延迟可能比一次罕见错误带来更大损失。

Axiom 的绝对正确性，在追求速度的金融场景中，其实际价值目前仍需要打一个问号。另一个挑战，则在于除了对价格不敏感的航空航天、国防军工等少数领域，其他绝大多数企业愿意为 " 绝对正确 " 支付高溢价吗？

洪乐潼自己也承认这一点：" 数学怎么赚钱？我们从一开始就面临这个挑战。" 但她认为，" 现在，商业信号已经清晰很多，数学能创造价值，是因为它能自我验证、自我检查。"

另一方面，高估值本身也是一把双刃剑。16 亿美元的 A 轮估值意味着，投资人期望的是超高速的增长和明确的退出路径。

Axiom 必须在未来一到两年内证明其技术具备规模化商业化的可能，否则下一轮融资将面临巨大压力。与此同时，它需要在巨头和强劲对手的夹击中，用更少的资源跑出更快的速度。

Axiom 的未来，更像是一场理想主义的压力测试。 从 " 绝对正确 " 的技术理想，到 " 相对经济 " 的商业世界，Axiom 的挑战，才刚刚开始。