成立不到一年，估值16亿美元。Axiom这轮融资由Menlo Ventures领投，老股东全员跟投。但比数字更扎眼的，是创始人洪乐潼——一个25岁的潮汕姑娘，正在用大模型最缺的东西换钱：确定性。
洪乐潼的履历像被按了快进键。广州普通家庭出身，17岁进MIT，三年拿下数学与物理双学位，顺手发了9篇论文。罗德奖学金、摩根奖、Schafer数学奖——这些名字堆在一起，足够在学术圈躺平一辈子。但她偏偏在斯坦福读博时退学了。
退学的原因很产品经理：她看到了AI行业最拧巴的bug。大模型越来越能聊，却越来越不敢信。日常聊天胡说八道顶多尴尬，放到对冲基金或国防系统里，概率性的"大概对"就是灾难。去年ChatGPT o3被质疑"数学测试作弊"时，洪乐潼第一个站出来戳破窗户纸：现在的AI根本没有严格的逻辑推理训练，全是统计规律堆出来的幻觉。
她的解法是把数学家那套搬进AI。Axiom的系统不用概率猜答案，而是用Lean语言生成可机器验证的证明过程。传统大模型给你结果，你只能选择信或不信；Axiom给你结果，同时附赠一份完整的形式化证明，每一步都能查、能验、能追责。
去年12月的普特南竞赛是个漂亮的demo。这个北美最虐的大学生数学竞赛，中位数常年为零，近百年只有5人拿过满分。Axiom的AI系统12题全对。更狠的是，它还用可验证的方式证明了一个存在20年的数论猜想——连Axiom的创始数学家Ken Ono都曾多年啃不下来。
Ken Ono的名字值得单独说。弗吉尼亚大学终身教授、美国数学学会前副主席、古根海姆奖得主，还是唯一出演过百威超级碗广告的数论学家。去年12月，他辞去教职全职加入Axiom。一个功成名就的学术大佬，为一个25岁的前学生打工。华尔街日报说，这位曾对AI嗤之以鼻的怀疑论者，"见到系统后顿悟了"。
团队里还有Meta AI前研究总监Shubho Sengupta，以及最早把Transformer引进数学领域的François Charton。一位投资人评价洪乐潼：数学功底、运营效率、聚人能力——二十年硅谷生涯里，最印象深刻的创始人，没有之一。
洪乐潼在朋友圈写过一句自勉：祝自己做花也做树。缤纷热情，孤离兀立。这话放在Axiom身上倒也贴切——既要像花一样吸引顶尖人才，又要像树一样在"可验证AI"这条窄路上扎下根来。
她的终极野心不止于修补AI的可靠性漏洞。"Verified AI瞄准的是AI的上限，是通向超级智能的阶梯。"换句话说，她想让数学证明的严谨性，成为AI突破天花板的基础设施。
从广州走出的女孩，到让终身教授辞职追随的创业者。洪乐潼这一代00后正在改写硅谷的剧本：不是为了追风口而创业，是为了解决真正困难的技术问题。当Axiom的下一个客户签下合同时，合同里大概会多一条别处见不到的条款——证明过程需随交付物一并提供。
热门跟贴