打开网易新闻 查看精彩图片

AI行业有个公开的秘密：大模型越聪明，撒谎越像真的。

ChatGPT能写论文、能编程、能解奥数，但没人能保证它到底是算出来的，还是蒙对的。就像考试时那个永远提前交卷的同学——分数很高，但你不敢抄他的答案，因为不知道哪一步是瞎编的。

洪乐潼想做的，就是给AI的每一步推理装上"行车记录仪"。

这个24岁的广东女孩，17岁进MIT，三年拿下数学物理双学位，斯坦福博士读到一半退学创业。公司Axiom成立不到两年，20来号人，最近A轮融资2亿美元，估值16亿美元——折合人民币110多亿。

她不做聊天机器人，不做文生图，专啃一块硬骨头：用数学证明AI没撒谎。

这事听起来像给龙卷风装刹车片。但洪乐潼的逻辑很直接：现在AI最大的痛点不是不够强，是不够可靠。金融风控、自动驾驶、芯片设计这些场景，错一次就是灾难。而Axiom要做的，就是把AI从"概率黑盒"变成"可验证的白盒"——每一步推理都能被数学严格检查，错了就当场抓包。

她的工具是一种叫Lean的编程语言。普通数学证明写5000行，得找专家逐行验算；Lean是自验证的，跑通了就是对的。Axiom的玩法是让大模型负责猜和搜，Lean负责审和判，审不过就退回去重算。

这条路冷到什么程度？全球商业化玩家一只手数得过来。洪乐潼去融资时，投资人问得最多的是："数学怎么赚钱？"

但她偏偏对"困难"上瘾。"奥数像持续释放多巴胺，研究型数学像在撞墙，充满痛苦与煎熬。我特别喜欢这种挑战感。"

这种性格也体现在组团队上。Axiom的CTO是Meta AI前研究总监，核心科学家是把Transformer引进数学推理的先驱，最新加入的是57岁的数学泰斗小野健——弗吉尼亚大学终身教授，美国数学学会前副会长，带过十个摩根奖得主。这位曾拒绝Google和Meta的老先生，愿意给24岁的前学生"打工"，条件是"不设教学、不设行政、100%科研"。

洪乐潼管这叫"草根工程师精神"。她解释：不是背景草根，是心态空杯。"我自己最喜欢的不是当精英，而是做nobody，这样学习的坡度最陡。"

2025年底，这支"草根"团队交出成绩单：AxiomProver无人干预下攻克两道困扰数学界数十年的埃尔德什难题，又在普特南数学竞赛拿下满分——这项北美最负盛名的大学生赛事，百年仅5位人类选手满分，中位数常常是零。

但商业化的问号还在。洪乐潼最初想服务对冲基金，但高频交易要的是"足够快"而非"绝对对"，毫秒延迟比罕见错误更致命。除了航空航天、国防军工等少数对价格不敏感的领域，多数企业愿为"绝对正确"付多少溢价，仍是未知数。

16亿美元估值意味着投资人要的是超高速增长。Axiom必须在两年内证明规模化商业化的可能，同时在巨头夹击下用更少资源跑得更快。

从"绝对正确"的技术理想到"相对经济"的商业世界，这场压力测试才刚刚开始。而洪乐潼的回应是：她仍在斯坦福附近那家咖啡馆办公，步行半小时就能回到那个没读完的博士项目——只是现在，她连回去的路都懒得记了。