一位25岁的广州姑娘，从斯坦福博士退学创业，带领20人团队在不到两年时间里将公司估值推至110亿美元——这听起来像是硅谷又一出创业传奇。然而真正令人惊讶的，并非她的年龄，而是她所深耕的方向：既不是聊天机器人，也不是AI绘画，而是专门攻克大模型最棘手的“幻觉”问题。用她自己的话说，就是“从数学根源上封住AI胡说八道的嘴”。

2026年3月中旬，洪乐潼创立的AI公司Axiom完成了2亿美元A轮融资，估值直接飙升至110亿美元，稳居独角兽行列。消息传出后，硅谷风投圈几乎沸腾——要知道，这家公司成立至今仅两年，团队仅有20人。更绝的是，他们不追逐任何热门应用赛道，只专注一件事：用形式化验证技术，确保AI的每一条推理都经得起数学检验。

具体如何实现？Axiom采用了一种“异构协作”模式：大模型负责猜想与搜索，Lean编程语言负责最终验算。任何一步逻辑跳跃，系统都会直接拒绝通过。听起来简单，但这正是当前业内解决AI可信问题最硬核的路径之一——不是试图训练模型“更诚实”，而是从逻辑底层把漏洞彻底焊死。

效果如何？2025年12月，Axiom的核心系统AxiomProver在普特南数学竞赛中完成了全部12道试题并拿下满分。这可是全美最顶尖的本科生数学竞赛，近百年来仅有5位人类选手达成过满分成就。同月，洪乐潼入选了“福布斯30岁以下30人”榜单。对于一位退学创业的博士生而言，这份认可来得既快且猛。

洪乐潼的履历本身就是一部“天才说明书”。2001年出生于广州一个普通务工家庭，17岁考入麻省理工学院，三年内修完数学与物理双学位。本科期间发表9篇论文，拿下北美数学本科生最高荣誉摩根奖，还获得美国每年仅授予一名女性本科生的Alice T. Schafer数学奖。2024年，她凭借罗德奖学金赴牛津攻读神经科学硕士，随后进入伦敦大学学院盖茨比计算神经科学中心投身深度学习研究。之后又考入斯坦福攻读数学与法律双博士——直到最终选择退学创业。

从MIT到牛津再到斯坦福，洪乐潼的每一步都踩在学术金字塔的顶端。但她选择在最该埋头写论文的年纪，把赌注押在了一个极其冷门却又极为关键的方向上。Axiom的成功，某种程度上代表了市场对“高确定性AI”的渴望——当大模型铺天盖地而来时，谁先解决了“它到底靠不靠谱”这个核心问题，谁就拿到了下一张船票。而这张船票，洪乐潼和她的20人团队，已经紧握在手。