新智元报道
编辑：倾倾
【新智元导读】2亿美元A轮融资，估值110亿，成立仅一年就成为独角兽。更震撼的是创始人——25岁的广州00后洪乐潼，父母是从未上过大学的普通务工者。她用数学解决AI最大的痛点：让模型推理步步可验证，彻底杜绝幻觉。为了加入她，弗吉尼亚大学终身教授直接辞职。
就在上周，全球创投圈被一个名字刷屏了。
AI初创公司Axiom宣布完成2亿美元A轮融资，由硅谷顶级风投Menlo Ventures领投，Greycroft、Madrona Venture、B Capital、Toyota Ventures等老股东全部跟投。公司估值飙升至16亿美元。
成立不到一年，直接跻身独角兽。
但更让人震撼的，是这家公司的创始人——25岁的洪乐潼（Carina Hong）。
她让大模型的推理过程像数学证明一样严格，每一步都可验证。
17岁进MIT，3年修完双学位
洪乐潼祖籍潮汕，出生在广州，父母是普通务工者，但她从小就展现出极其罕见的数学天赋。
高一时，她入选广东省中学生英才计划，师从中山大学教授王学钦。
随后，她在全国中学生数学奥林匹克（CMO）广东选拔中脱颖而出，成为仅有的四位女生之一。
2018年，17岁的洪乐潼被麻省理工学院（MIT）录取，选择了数学与物理双专业。
接下来的履历，堪称「开挂」。
她在MIT只用3年就修完两个学位，本科期间发表了9篇学术论文，研究方向涵盖模椭圆曲线、K3曲面上的L函数、「月光猜想」等基础数学领域。
她曾获得全美女性数学家最高荣誉——Alice T. Schafer数学奖，以及表彰北美数学专业本科生杰出研究的AMS-MAA-SIAM摩根奖 。
2021年，洪乐潼获得牛津大学罗德奖学金，成为当年仅有的四位中国获奖者之一。
罗德奖学金被誉为「本科诺贝尔奖」，是世界上历史最悠久、最负盛名的国际奖学金项目。
在牛津攻读神经科学硕士期间，她在伦敦大学学院盖茨比计算单位作为第一作者开展深度学习研究，正式踏入AI领域。
随后她又进入斯坦福大学，攻读数学与法律双学科博士。
但博士还没读完，她就退学了。
AI的致命缺陷：概率模型没有「绝对正确」
洪乐潼看到的，是AI行业最尖锐的矛盾。
大模型的能力在狂飙，但可靠性始终是个黑盒。
日常应用中的胡说八道或许无伤大雅，但在金融、国防、关键基础设施领域，任何基于概率的错误都可能酿成灾难。
去年针对ChatGPT o3「数学测试作弊」争议，作为斯坦福数学博士的洪乐潼率先指出症结：当前AI缺乏严格的逻辑推理训练体系。
现有的大模型本质上是概率机器。它们通过海量数据学习模式，然后基于统计规律给出答案。
即使是GPT-4、Claude这样的顶级模型，其概率性的本质依然是主要的担忧原因。
洪乐潼的答案是：让AI像数学家一样工作。
她创立的Axiom采用「数学即服务」模式，通过训练AI系统生成用Lean语言编写的、经过形式化验证的输出。
Lean是一种专为数学证明设计的编程语言，通过使用Lean，Axiom可以确保AI模型推理过程的每一步都是可机器检查的并且在逻辑上得到保证。
传统大模型给你一个答案，你只能信或不信。而Axiom的系统给你一个答案，同时附带一个完整的、可验证的证明过程，不存在大概是对的这种模糊地带。
洪乐潼在接受采访时说：
科学突破往往需要两步：提出假设，再用证明去验证。我们创立Axiom，就是要无限压缩把好奇心转化为真理的时间。
满分通过普特南竞赛，攻克20年数论猜想
去年12月，Axiom交出了第一张成绩单。
Axiom的核心系统在普特南竞赛中，斩获满分，12题全对。
普特南竞赛是北美地区最负盛名的大学生数学竞赛，成绩的中位数常常为零（满分120分）。
过去近百年，仅有5人达成过满分成就。Axiom的AI做到了。
更震撼的还在后面。Axiom可验证地证明了一个已有20年历史的数论猜想，该猜想涉及用于测量曲面距离的微积分元素。
这个问题，连Axiom的创始数学家Ken Ono都曾多年尝试未能解决。
去年12月，Axiom开发的AxiomProver系统，使用可验证的Lean语言，完成了埃尔德什问题集中第124题和第481题的形式化证明，分别用时1天和5小时，全程无人为干预。
埃尔德什问题集共包含1109个关于组合数学和数论的问题，是匈牙利数学家保罗·埃尔德什数十年来论文的汇集。
迄今为止，只有266个问题被证明，其中仅10个问题的证明被转化为计算机可验证的形式化版本。
解决数学问题只是冰山一角。Axiom正在将这种「绝对正确」的数学推理能力，通过迁移学习引入到代码验证领域，试图解决生成式AI的种种问题。
目标客户是对冲基金、量化交易员等高端场景。这些地方，容不得半点「大概对」。
终身教授辞职加入，只因「见证了数学超级智能的可能」
Axiom最震撼的一次招聘，发生在去年12月。
Ken Ono（小野健），弗吉尼亚大学Marvin Rosenblum讲席教授、前美国数学学会副主席，辞去终身教职，全职加入Axiom担任创始数学家。
他是古根海姆奖、帕卡德奖、斯隆奖得主，世界顶尖的拉马努金数学权威之一 ，还是电影《知无涯者》的副制片人和数学顾问，甚至出演过百威啤酒的超级碗广告。
并且，他也是唯一一位出演过啤酒广告的数论学家。
在Ken Ono长达四十年的执教生涯中，曾指导过十位摩根奖得主，洪乐潼正是其中之一。
为什么一个功成名就的终身教授，会放弃稳定的学术生涯，去为一个25岁的年轻人工作？
华尔街日报报道称，Ken Ono在人工智能彻底改变他的职业生涯和生活之前，一直对人工智能持怀疑态度。
直到最近，他开始谈论人工智能时，还总是嘲讽围绕这项新兴技术的炒作 。
但见到Axiom的系统后，他顿悟了。
除了Ken Ono，Axiom的团队堪称「梦之队」：
CTO Shubho Sengupta曾任Meta AI研究总监，此前参与过Google分布式训练系统的研究工作，也是最早开发CUDA技术的专家之一 ；
核心科学家François Charton，是率先将Transformer模型引入数学领域的先驱，曾用大模型推翻过一个长达30年未解的学术猜想。
一位投资人忍不住感慨：
她兼具深厚的数学功底、惊人的运营效率，以及吸引世界一流人才的能力。这是我过去二十年的硅谷生涯中，见过的最令人印象深刻的创始人，没有之一。
目前，Axiom拥有30多名员工，招聘速度还在不断加快。
00后集体登场，AI创业进入「理想主义者」时代
就在上周，成立仅一年多的公司灵初智能宣布完成天使轮及Pre-A轮共计20亿元融资。
其联合创始人陈源培，出生于2001年，曾就读于北京大学、斯坦福大学，师从李飞飞。
同为00后的杨丰瑜在耶鲁博士毕业后选择回国创业，2024年成立了具身智能公司优理奇，完成数亿元的天使轮及天使+轮融资。
2025年，由三位00后创立的AI招聘网站Mercor也宣布完成1亿美元的B轮融资，公司估值达20亿美元。
这一代创业者，和上一代有什么不同？
曾在DeepSeek火爆全球之际，洪乐潼发出这样的感慨：
一个小而专注、特立独行的团队。一群理想主义者组成的优秀合作伙伴。他们执行力强，亲力亲为。最珍贵的，是那份理想与使命交织的信念。这就是DeepSeek的故事，也是我想亲自书写的故事。
有投资人私下交流时回忆，洪乐潼在创立Axiom期间于朋友圈写下的自勉：
祝自己做花也做树。缤纷热情，孤离兀立。
谈话间，她几乎不谈论风口与颠覆，更多在意对问题本身的好奇和对技术可能性的清晰判断。
对于Axiom的终极使命，洪乐潼留下了一句极具张力的注脚：
Verified AI关注的，绝不仅仅是修补AI的缺点。真正瞄准的，是AI的上限，是通向超级智能的阶梯。
从广州普通家庭走出的女孩，到掌舵估值110亿的AI独角兽。
从MIT的数学天才，到让终身教授辞职追随的创业者。
洪乐潼和她这一代00后创业者的故事，正在改写硅谷的叙事规则：不是为了风口而创业，而是为了解决真正困难的技术问题。
AI的上限在哪里？或许答案就藏在这群25岁年轻人的选择里。
参考资料：
https://mp.weixin.qq.com/s/msJXxZMSyfXMXDPMCdtznQ
热门跟贴