那个从华附走出去的姑娘，在硅谷改写了AI的"信任规则"

2026年春天，硅谷流传着一个关于"信任"的故事。一位25岁的广州姑娘，用不到一年时间，让一家AI公司估值突破百亿人民币。她的方法很特别——不是让AI变得更聪明，而是让它变得"可被相信"。

故事的主角叫洪乐潼。要理解她做了什么，得先从我们熟悉的AI困境说起。用过ChatGPT的人都知道，它偶尔会"一本正经地胡说八道"。这种小毛病在聊天时无伤大雅，但如果AI要帮银行算一笔百亿交易，或者帮医院诊断病情呢？一个基于概率的"可能正确"，在关键场景里就是一颗定时炸弹。

洪乐潼在牛津读硕士时，第一次深刻感受到这种矛盾。她在盖茨比计算单位做深度学习研究，发现再精妙的模型，底层都是统计游戏——猜对了加分，猜错了下次调整。这种机制天生带着不确定性。而她从小迷恋的数学，恰恰是另一套逻辑：一个命题，要么对，要么错，没有中间地带。

能不能让AI像数学证明一样工作？每一步都有据可查，每一个结论都经得起推敲？这个想法在她脑海里盘旋多年，直到2024年那个深秋的午后，在斯坦福附近的一家咖啡馆里，终于找到了落地的可能。

从一杯咖啡到一支改变规则的团队

那天，洪乐潼约见的是MetaAI研究总监ShubhoSengupta。两人聊了几小时，话题越来越聚焦：如果AI能解决世界上最难的数学问题，它首先要学会"证明自己是对的"。这场对话结束后不久，洪乐潼做出了一个让身边人惊讶的决定——从斯坦福退学，创立Axiom。

ShubhoSengupta成了她的第一位合伙人，现任CTO。更戏剧性的是，她MIT时期的导师、57岁的数学泰斗小野健，听闻昔日学生的创业方向后，毅然辞去弗吉尼亚大学的终身教职，加入了这支20多人的小团队。

小野健是谁？模形式领域的顶尖学者，美国数学学会前副会长，拿过古根海姆奖、斯隆奖，曾为美国奥运游泳队做数据分析，还给电影《知无涯者》当顾问。这样一位功成名就的学者，选择追随一个25岁的姑娘重新出发——这本身就说明了一些事情。

Axiom做的事情，用行话叫"形式化验证"。简单说，就是用一种叫Lean的编程语言，把数学证明变成可执行的程序。AI生成的每一行代码、每一步推理，都要经过严格的逻辑检验，像解几何题一样，不能跳步，不能含糊。

效果在2025年底得到验证。Axiom的系统参加了被誉为"本科生数学奥林匹克"的普特南竞赛，12道题全对满分。近百年来，只有5个人类做到过。随后，它又独立证明了多个数论领域的开放猜想。

资本押注的背后：一场关于"确定性"的共识

2024年8月，Axiom拿到960万美元种子轮。5个月后，A轮融资2亿美元，估值16亿美元。领投方MenloVentures的合伙人MattKraning说了一句话，点破了资本的热情所在："我们正步入一个AI几乎可以编写所有软件的世界，但几乎没人提一个问题——这些代码都没被验证过，这是巨大的风险。"

洪乐潼的回应很朴素："Axiom很小，却很强。我们在探索更聪明的技术来降低成本，资本效率很高。"这笔钱一部分用于算力，一部分用于招人。已经有对冲基金和量化交易公司找上门来——他们需要解决的资产定价、股市预测问题，恰恰最需要"确定性"。

面对同样专注数学AI的竞争对手Harmonic，洪乐潼并不焦虑。对方花了两年多达成第一个重要里程碑，而Axiom的节奏快得多。她更在意的，是技术理想本身能否持续。

2025年，DeepSeek横空出世。洪乐潼评价那群同行："理想主义者组成的优秀伙伴，执行力强，亲力亲为。最珍贵的，是理想与使命交织的信念。"她说，这也是她想亲自书写的故事。

从华附的奥数赛场，到MIT的双学位，再到牛津的跨界探索，最后落脚于硅谷的创业征程——洪乐潼的路径看似跳跃，内核却始终如一：用数学的严谨，给狂飙的AI系上安全带。这个故事的启示或许在于：在技术狂热中，"慢下来验证"本身，就是一种稀缺的价值。