初创公司 Axiom Math 由 24 岁的 Carina Hong 创立，致力于开发能够自主验证逻辑正确性的“AI 数学家”。该公司在 2025 年获得 6400 万美元融资，核心团队汇聚了来自 Meta 和 Google 的顶尖人才以及知名数学家。与主流大模型不同，其系统通过 Lean 编程语言确保推理过程的每一步都可追溯、可检查，解决了 AI 产出结果难以验收的信任难题。通过在 Putnam 数学竞赛中的优异表现，Axiom 证明了 AI 可以从简单的答案生成转向严密的形式化证明。这种对可信度的追求，旨在将 AI 从不稳定的辅助工具提升为能在科研与工业领域真正落地、可被验收的可靠合作者。

2025 年，几乎每一场 AI 发布会都在说“我们能做什么”。

但企业真正卡住的，是另一个问题：AI 做出来的结果，怎么证明是对的？

很多 AI 产品上线前 demo 演示得很好，一上线就出问题： 

错误定位不了， 

责任追不清楚， 

结果复现不了。

最后只能说：没法验收。

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

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