25岁潮汕女孩让AI"自证清白"，数学教授为她辞去终身教职

成立不到一年，估值16亿美元。Axiom这家AI公司的融资消息，像极了硅谷版的"开局即巅峰"。

但真正的爆点藏在创始人身上——25岁的洪乐潼，一个从广州普通家庭走出的潮汕女孩，正在用大模型的"数学洁癖"挑战整个行业的底层逻辑。

她的解题思路很直接：既然AI胡说八道的毛病治不了，那就让它的每一步推理都能被查验。

洪乐潼的履历读起来像开了倍速。高一时入选广东省英才计划，17岁进MIT，三年拿下数学与物理双学位，本科期间发了9篇论文，研究方向从模椭圆曲线到"月光猜想"，全是基础数学里让人头皮发麻的领域。罗德奖学金、摩根奖、全美女性数学家最高荣誉——她拿了个遍。

转折点发生在牛津。攻读神经科学硕士期间，她第一次系统接触深度学习，随即发现那个让从业者集体装睡的问题：大模型本质是概率机器，统计规律堆出来的"聪明"，在关键领域就是颗定时炸弹。

金融交易、国防系统、基础设施——这些地方容不得"大概对"。ChatGPT o3的"数学作弊"争议更是让她确信：没有严格逻辑训练的AI，再强也是空中楼阁。

她的解法堪称叛逆——让AI像数学家一样工作。

Axiom的核心是"数学即服务"。系统用Lean语言生成输出，这是一种专为数学证明设计的编程语言，每一步推理都可被机器查验、逻辑上完全保证。传统模型给你答案，你只能选择信或不信；Axiom给你答案的同时，附赠一份完整的"验货报告"。

去年12月的普特南竞赛是个漂亮的亮相。这个北美最负盛名的大学生数学竞赛，成绩中位数常常是零分，近百年只有5人拿过满分。Axiom的AI12题全对。

更狠的是后续操作：AxiomProver系统用Lean语言，在1天和5小时内分别搞定埃尔德什问题集中的两道难题，全程无人干预。这个汇集1109道组合数学与数论难题的题库，至今只有266道被解决，其中仅10道完成了计算机可验证的形式化证明。

团队阵容同样不讲道理。CTO Shubho Sengupta是Meta AI前研究总监，CUDA技术的早期开发者；核心科学家François Charton率先把Transformer引入数学领域，曾用大模型推翻一个悬置30年的猜想。

最戏剧性的招募发生在去年12月。Ken Ono，弗吉尼亚大学讲席教授、前美国数学学会副主席、古根海姆奖得主，辞去了终身教职。这位世界顶尖的拉马努金研究权威，此前对AI炒作嗤之以鼻，直到亲眼见到Axiom的系统。

他指导过十位摩根奖得主，洪乐潼是其中之一。现在，他为曾经的学生打工。

洪乐潼在朋友圈写过一句自勉：祝自己做花也做树。缤纷热情，孤离兀立。这话放在Axiom身上倒也贴切——既要像花一样吸引顶尖人才，又要像树一样在技术深处扎根。

她的终极野心写在公司使命里：Verified AI不是要修补AI的缺点，而是瞄准AI的上限，通向超级智能的阶梯。

当同龄人还在讨论风口与颠覆时，这位25岁的创始人只在意两件事：对问题本身的好奇，和技术可能性的清晰判断。换句话说，她选了一条最难的路，因为容易的路解决不了真正困难的问题。

一位投资人在内部交流时评价：这是我二十年硅谷生涯里，见过最令人印象深刻的创始人，没有之一。