25岁广州少女获14亿融资！斯坦福辍学，要用数学公理改写AI代码

2026年3月中旬，硅谷AI圈被一位广州女孩彻底刷屏。 由25岁天才少女洪乐潼（Carina Hong）创办的AI初创公司Axiom宣布完成2亿美元（约14亿元人民币）A轮融资，领投方为顶级风投Menlo Ventures。公司成立不足两年，团队仅20人，估值已飙升至110亿元人民币，正式跨入全球独角兽行列。

从华附到斯坦福：天才少女的“快进”人生

洪乐潼的履历，是典型的高频“跳级”范式。1999年出生于广州，高中就读于享有盛名的华南师大附中，曾是奥数省队成员，骨子里刻着深厚的数学基因。

• 学术收割机： 本科仅用三年便拿下MIT数学与物理双学位，随后在牛津大学跨学科攻读神经科学硕士，并摘得2022年中国罗德奖学金。
• 果断辍学： 2024年，她进入斯坦福大学攻读数学与法学双博士。然而，面对AI浪潮的爆发，她直言“等不了毕业”，入校仅几个月便决定辍学，在硅谷帕洛阿尔托租下办公室开启创业之路。

降维打击：不卷对话模型，只为代码找“公理”

在主流AI公司沉迷于聊天机器人和文生图时，洪乐潼选择了一条极其硬核且高门槛的赛道——形式化验证（Formal Verification）。

Axiom的核心逻辑不再是让AI去“猜”下一个单词，而是让AI像数学家证明定理一样，自动检查代码逻辑。其自研系统AxiomProver的表现堪称恐怖：

• 竞赛降维打击： 在2025年12月的普特南数学竞赛中夺得120分满分。
• 攻克世界难题： 该系统独立证明了悬而未决30年的埃尔德什问题#124，以及尘封45年的问题#481。

通过Lean编程语言，Axiom正在为代码构建一套底层“公理”，试图从源头彻底杜绝Bug的存在。

资本狂欢：2亿美元背后的“自我验证”逻辑

本轮2亿美元的巨额融资，由Menlo Ventures领投，Greycroft、Madrona等机构跟投。这不仅是对洪乐潼个人的加冕，更是资本对AI下半场逻辑的押注。

领投方Menlo Ventures分析称： “AI生成代码正在普及，但准确性是致命瓶颈。Axiom能从底层逻辑杜绝错误，这是大模型商业化落地的‘刚需’。”

洪乐潼对此回应极其客观克制： “数学之所以有价值，是因为它能自我验证、自我检查。我们的目标是降低算力成本，提高资本效率。”

豪华配置：20人团队撑起百亿估值

Axiom团队只有20多人，但背景堪称“豪华”：

• CTO Shubho Sengupta： 前Meta AI研究总监；
• 核心成员小野健（Ken Ono）： 辞去弗吉尼亚大学终身教职加入；
• François Charton： 前Meta AI研究科学家。

团队中约一半成员曾供职于Meta AI实验室。这种“顶尖导师+工业界大牛”围绕天才少女组建的架构，保证了公司在数学理论与AI工程化上的双重领先。

行业影响：软件工程与金融市场的“地震”

Axiom的技术落地，其想象空间远超普通大模型：

1. 重构软件生态： 若AI自动证明代码正确性，传统人工测试环节将面临结构性改变，软件崩溃、系统漏洞或将成为历史。
2. 颠覆量化金融： 洪乐潼曾透露，产品未来将服务于对冲基金，解决极其复杂的资产定价与股市预测模型。
3. 人才信号意义： 从国内华为“天才少年”到洪乐潼的硅谷突围，中国数学教育背景正成为全球AI前沿竞争中最核心的底座。

后续走向：随着14亿元融资到账，Axiom接下来的重点将集中在扩充算力资源与争夺顶尖人才上。这位25岁的广州女孩能否用数学“公理”改变世界？答案也许就藏在下一行被验证的代码里