AI数学家Axiom Math：24岁创始人Carina Hong与她的可信AI革命

由24岁华裔创业者Carina Hong领衔的初创企业Axiom Math，正致力于打造能够自主验证逻辑严谨性的“AI数学家”。该公司于2025年成功募集6400万美元资金，其核心团队汇集了来自Meta和Google的人工智能专家以及著名数学家。与传统大型语言模型不同，Axiom的系统采用Lean编程语言，确保每一步推理均可追溯和检查，从而破解了AI输出结果难以验收的信任难题。通过在Putnam数学竞赛中的出色表现，Axiom证明了AI能够从简单的答案生成跃升至严密的形式化证明。这种对可信度的执着追求，旨在将AI从不够稳定的辅助工具转变为能够在科研和工业领域真正落地、可被验收的可靠伙伴。

2025年，AI发布会几乎都在高喊“我们能做什么”。

然而，企业真正面临的瓶颈是另一个问题：AI给出的结果，如何证明其正确性？

众多AI产品上线前演示完美，一旦投入实际应用便问题频发：

错误无法定位，

责任难以追溯，

结果无法复现。

最后只能得出一个结论：无法验收。

Axiom Math，一家总部位于旧金山的AI初创公司，另辟蹊径：不追求AI能做什么，而是证明它做对了什么。

这家刚在2025年10月完成种子轮融资（6400万美元，估值3亿美元，B Capital领投）的公司，正在打造一位AI数学家，既能独立给出答案，也能自行验证对错。

正因如此，这个团队吸引了一批技术底蕴深厚的人才：来自Meta FAIR、Google Brain的前核心研究员，以及创始人Carina Hong在MIT的导师、著名数学家Ken Ono。

Carina Hong，24岁。

2025年12月21日，有媒体问及她的招聘秘诀，她回答得简洁明了：

问题够难，人自然会聚过来。

这并非空谈。她的策略就是找到一个值得投入十年去攻克的难题，然后等待真正的高手主动上门。

24岁，6400万美元，估值3亿。

她押注的不是一个产品，而是AI的下一个及格线。

第一节｜24岁，3亿估值，她要让AI学会自证

她叫Carina Hong，出生在广州。

童年解奥数题时，她未曾想到自己未来会站在硅谷讲述AI的故事。但她记得，每解开一道题，就像孩子通关游戏，欲罢不能。

她一路从广州考入MIT，再获罗德奖学金赴牛津攻读神经科学，最后进入斯坦福攻读数学博士+法学博士联合项目。

在MIT，她修读了20门研究生数学课程，发表了9篇论文，还研究了神经网络如何理解函数。在牛津，她待在UCL盖茨比研究所（DeepMind的诞生地），首次近距离观察AI解决真实问题：图像识别、序列建模、控制优化。

她开始自问：如果AI能玩游戏、能写代码，为何不能做数学？

真正的转折发生在硅谷。

她在斯坦福读博期间，常去一家咖啡馆写论文。一次偶然的机会，她结识了Meta FAIR团队的AI科学家Shubho Sengupta。

一个是数学家，渴望让AI理解数学。

一个是工程师，希望找到AI真正值得解决的问题。

他们畅谈两小时，没有谈论项目，也没有涉及融资，只围绕一个假设展开：能否造出一位AI数学家？

那次对话后，她开始认真思考这件事。不久，她退学了。

她说：有些问题，在学校里解决太慢了。

她要做的，不是聊天机器人，也不是代码助手，而是一个能验证定理、甚至提出新猜想的AI系统。

这个系统名为Axiom，意为“公理”，即数学理论最基础的起点。

从这个起点出发，开发一整套系统，让AI也能探索数学的边界。

第二节｜Putnam考试9/12，但重点不是分数

大多数人理解AI学数学，想到的往往是考试、给答案。

但Carina说，那只是第一步。真正重要的，是它是否知道自己答得对不对。

这不仅关乎数学，也是工程挑战。AI的答案如果不能被验证，就无法用于关键场景。

人类做数学题，有个天然优势：我们可以回头检查，看证明是否有逻辑漏洞，推理有无跳步，细节是否一致。

Carina把这种检查过程称为“验收”。

但大模型做不到。

它们能生成大量内容，却很难自我确认这些内容是否正确。尤其在数学领域，哪怕多一个字母，整个结论就可能崩塌。

要解决这个问题，必须依靠形式化语言。

Carina的团队采用一种名为Lean的数学编程语言。所有公式、步骤、证明，必须像程序一样清晰书写，并且能够通过机器验证。

这意味着，不是AI说对就算对，而是它每走一步都要留下可检查的痕迹，最终像软件测试一样通过验证。

为了验证这套方法的可行性，他们进行了一次测试。

2025年12月，美国Putnam数学竞赛落下帷幕，这是全美难度最高的本科生数学竞赛，参赛者约4000人。Carina团队在X平台上发布结果：AxiomProver自主解出其中9道题，并用Lean语言给出了形式化证明，全部通过验证。

这不仅仅是做对9道题，而是AI自己解题、自己检查、自己确认通过。

Carina说：

“我们追求的不是一个能抄答案的AI，而是一个能完成所有数学细节的合作者。”

验收的真正含义是什么？

就是AI不仅要给出答案，还要证明答案是对的。

在芯片设计、科学研究、金融系统这些容错率极低的场景中，模糊的答案毫无价值。AI必须能呈现过程、解释思路、接受检验。

能被验收，才意味着能被信任。

第三节｜Meta、Google的人为什么离职来这里

要实现这一目标，需要怎样的团队？

这个团队目前仅17人，但每一位都是各自领域的顶尖研究者。

CTO Shubho Sengupta，是Carina在斯坦福附近咖啡馆偶遇的。他曾在Meta FAIR带队开发OpenGo和CrypTen，也参与过早期CUDA GPU架构设计。他深知大模型的局限，也明白数学领域的特殊挑战。

但在大公司，目标过于分散。他渴望找到一个地方，专注解决一个极限难题。

另一位核心成员François Charton，早在2019年就开始研究如何用Transformer解决积分问题。他注重细节，不关心大模型能生成多少内容，而是关注它是否会在某一步出错。

还有Hugh Leather，专注于深度学习与编译器的结合。他并非传统数学家，但在用代码表达复杂逻辑方面积累了深厚经验。

他们都从Meta、Google等大厂走出，放弃了更稳定的研究路径。

Carina提供的不是职位，而是一种愿景：用AI做出可验证的数学成果，每一步清晰，每个结论都经得起推敲。

这个愿景吸引的不仅是业界的AI研究员。

2025年12月初，57岁的数学家Ken Ono辞去了弗吉尼亚大学的终身教职，全职加入Axiom。

他曾是Carina的导师，领导过多个数学奥林匹克研究项目，是拉马努金理论的专家，也曾登上超级碗广告，将数论带入大众视野。

他说，作为纯数学家，他很少有机会参与改变世界的事。这一次，他不想错过，带着家人搬到硅谷，成为Axiom的第15位成员，身份是创始数学家。

他的任务不是写代码，而是设计难题，测试模型推理的极限。

Carina说，这些人之所以愿意来，并非追逐热潮，而是想做一件真正值得投入的事。

“我们不是在做一个产品，而是在定义一套新标准：每个公式都可检查，每道推理过程都可追溯。AI不是生成一个答案，而是展示完整的思考过程。”

这就是他们17个人正在做的事。

第四节｜不是解题，而是教AI提问

定义新标准，只是Carina的第一步。

她真正的目标是让AI学会发现问题本身。

他们最近在研究数学界一个著名的未解难题：Collatz猜想。这个问题看似简单如小学生游戏，却困扰了研究者数十年。

Axiom的研究员用Transformer模型学习这个问题，模型虽未能直接给出证明，但展现出了另一种能力：

在预测Collatz序列时，对万亿级数字的准确率达到了99.8%。

更重要的是，它为什么错、错在哪里，都能被清晰解释。这些错误背后存在明确的规律，而非随机的幻觉。

这意味着什么？

意味着AI不是在记忆答案，而是在学习数学思维。

在Carina看来，他们不是让AI寻找已知答案，而是训练它像一个真正的数学家那样去思考、去探索。

她所说的探索，主要分为三个阶段：

第一步，用形式语言表达定理，模仿已有的逻辑结构。

第二步，验证旧问题的不同解法，提出新的证明路径。

第三步，提出新猜想，创造从未出现过的问题并给出数学依据。

整个过程，不是ChatGPT式的随机对话，而是在证明空间里有规则地探索，不断尝试，直到发现新的路径。

这种探索为何重要？

因为数学是人类最严密的语言，也是现实世界运转的底层逻辑。每一个数学突破，都可能推动这些领域的飞跃。

Carina相信，数学研究曾以十年一进展的速度运行，现在AI可以把周期缩短到几个月。

而AI数学家未来能做的，不只是解题，更是与人一起重新定义问题本身。

这不限于数学领域。无论是密码学、芯片架构、物理建模，背后都依赖于能被精确描述与检验的数学原理。一旦AI做到可验证，它就能从“只能试试看”的辅助工具，变成“可以放心用”的合作者。

这，正是Carina在押注的那条线：

AI的下一个及格线，不是能力，而是可信度。

结语｜能被验收的，才叫AI

Carina的想法很简单。

她只给出一个判断标准：AI说得对不对，不是看有没有人信，而是看它能不能自己交代清楚。

Axiom Math所做的，就是让AI必须讲明白。不是让模型更像人，而是让它能被信任。

真正能用的AI，不靠Demo，靠验收。

这个标准一旦确立，AI走进科研、金融、芯片、法律，才算真正开始。

而她，只是把这扇门推开了一点点。

原文链接：

https://www.youtube.com/watch?v=b_UMhn8E8lI&t=264s

https://e.vnexpress.net/news/tech/personalities/building-math-ai-startup-how-24-year-old-stanford-dropout-carina-hong-is-attracting-big-tech-talent-4993367.html

https://www.businessinsider.com/axiom-math-stanford-dropout-meta-ai-researchers-startup-2025-12

https://www.turingpost.com/p/carina

来源：官方媒体/网络新闻