押注”数学超智能”——AI for Math赛道的公司、团队与资本地图
副标题：当Robinhood创始人、Putnam满分天才和陶哲轩同时押注同一个赛道时，这个赛道一定有什么东西你没看到。
2025年11月，Robinhood CEO Vlad Tenev做了一个让华尔街困惑的决定。
他的AI数学公司Harmonic完成了C轮融资——14.5亿。投资人包括Sequoia、Index、Kleiner Perkins，以及一个不那么寻常的名字：Nvidia。
他的金融科技公司Robinhood那年刚经历了meme股票风波的余震。但他几乎把所有业余时间都投进了Harmonic。
四个月后，2026年3月。一个24岁的斯坦福辍学生拿到了$2亿。她的名字叫Carina Hong。她的公司Axiom Math做的事情极度抽象：用Lean——一种专门写数学证明的编程语言——让AI生成可以被机器100%验证为正确的输出。
又过了三个月，Hack VC发表了一篇投资理论文章，解释了为什么投了Math Inc.—一家由前OpenAI科学家Jesse Han创立的公司——的理由。他们的核心论点只有一句话：
“正如没有芯片能不经Cadence验证就流片，未来没有AI生成的代码能不经形式化验证就上线。”
三家创业公司。不到两年时间。超过6亿美元公开融资。
一个全新的赛道正在诞生。它的名字叫”数学超智能”（Mathematical Superintelligence，MSI）。
而硅谷最聪明的钱，正在全力押注。
一、赛道的四层结构
AI for Math不是单一市场。它至少有四个层次——越往底层，技术壁垒越高，护城河越深。
第四层：AI数学教育
这是最”浅”的一层，但拥有最大的用户基数。
Photomath被Google以约100万+ARR和150万月活——零付费广告。Solvely AI有1000万+注册用户，App Store 4.7分。
这层的关键词是”拍照解题 + 步骤解释”。技术门槛不高，但用户粘性极强。所有人都在抢”下一个Duolingo for Math”的位置。
但这不是故事的核心。
第三层：形式化验证基础设施
这一层的公司不直接做”数学”，而是把形式化验证——一种曾经需要PhD手工艺级别的技术——变成工业级产品。
Theorem（4人，$600万种子轮，YC S25）：核心是”分数证明分解”——不是对整个代码库做全量验证（太贵了），而是按重要性比例分配验证资源。已在金融客户部署了16,000行AI生成代码——零人工审查上线。
Pramaana Labs（$2700万种子轮，Khosla/Accel/Nexus/Premji）：美国-印度双线作战。三个垂直领域：税务（与前IRS局长合作）、药物发现、网络安全。背后是IIT Delhi和IIT Madras的学术支撑。
Formel AI（法国，天使轮）：来自scikit-learn核心维护者和École polytechnique。四个形式化保证——100%逻辑一致性、可执行约束、完全可追溯、显著更低成本。
MerLean（预种子）：排名全球#5 Lean Eval Benchmark（小团队 vs 大公司）。专注量子计算形式化。
这一层的共有逻辑：AI正在产生大量代码和决策，而人类无法逐一验证。形式化验证是唯一的规模化解决方案。
第二层：中国力量
在这个赛道里，中国玩家的阵容不输硅谷。
TongGeometry（BIGAI/北大）：Nature Machine Intelligence 2026年1月封面文章。67亿几何定理。3道题入选真实竞赛。消费级GPU。最重要的是——它同时具备”发现”和”证明”的双重能力，这是全球独一份。
ByteDance Seed-Prover：IMO 2025金牌级（形式化验证）。
DeepSeek-Prover-V2：MiniF2F 88.9%。开源社区的标杆。
Moonshot AI的Kimina-Prover：MiniF2F 92.2%，首次证明了定理证明的scaling laws。
腾讯、上海AI实验室等也在布局。
中国力量的特点：大厂研究院 + 高校双轨制。发表的系统数量（至少7个）甚至超过美国。但TongGeometry是唯一发到Nature正牌期刊的中国AI数学系统——在”学术影响力”维度上，中国仍在追赶。
第一层：数学超智能——皇冠上的明珠
这是最深的一层。三家公司在争这个位置。
二、Harmonic：Robinhood创始人的第二幕
在硅谷，Vlad Tenev是一个有点矛盾的存在。
2021年初，Robinhood因为GameStop事件成为全美的焦点——说得好听叫”金融民主化”，说得不好听叫”散户赌场”。Tenev上了国会听证会。
2023年，他悄悄和Tudor Achim一起创办了Harmonic。Achim是Helm.ai的前CTO，在CMU学计算机，在斯坦福读博时辍学。
他们想做的不是”又一个AI公司”，而是数学超智能——一个所有输出都经过形式化验证的AI系统。
Harmonic的核心产品叫Aristotle。它的架构非常独特：
- 非形式层（直觉）：LLM阅读问题，生成高层次的证明策略——“这应该用归纳法”、“这个不等式可以放大”
- 形式层（严谨）：Lean 4搜索系统将策略翻译成严格的机器可验证证明
- 反馈循环：如果形式层验证失败，错误信息被送回非形式层，重新生成策略
这模仿了人类数学家的思维模式：先有直觉，再逐行验证，做错了就退回去重新想。
Aristotle在IMO 2025上解出了5/6题——金牌级。但更重要的是，它在训练过程中做了以下事情：
- 对Mathlib（全球最大开源数学库）做出了多个原创贡献
- 发现了陶哲轩教材中4道假设下为假的练习题
- 在一本流行教材中发现了错误
- 证明了范畴论和同调代数中超出竞赛范围的高级定理
Harmonic融资时间线：
- A轮$75M（Sequoia，2024年9月）
- B轮875M）
- C轮14.5亿）
Nvidia参与C轮这件事特别值得关注。表面上，训练数学AI需要GPU。但更深层的原因是：Nvidia需要AI被信任。 形式化验证 → AI代码安全 → 更多行业部署AI → 更多GPU需求。这是一个巨型企业的远期布局。
Aristotle已经公开发布了API和iOS App。20个人的团队，正在把”数学超智能”从研究概念变成商业化产品。
Tudor Achim在被问到”AI什么时候能在特定数学任务上超越人类”时，回答：
“2到3年内。不是有些人说的10年。“
三、Math Inc.：陶哲轩唯一合作的AI公司
Jesse Han的故事是AI数学界的传奇。
他在OpenAI担任高级研究科学家时，创建了GPT-f——历史上第一个被数学界正式接受为贡献的神经定理证明器。他还参与撰写了GPT-4技术报告。
他的博士导师是Tom Hales——那个花了20年形式化验证开普勒猜想的人（最终被认定为计算机验证数学的里程碑）。
Han离开OpenAI后创立了Math Inc.。产品叫Gauss——一个专注于”长证明”的自动形式化Agent。
为什么是”长证明”？因为竞赛级的短证明正在快速商品化——IMO题目被不同公司反复攻克。但研究级的长证明（数天计算、数十万行Lean代码）是一个完全不同的难度级别。
Gauss的成长曲线本身就是一道指数函数：
- 2025年6月：3,500行（de Bruijn定理）
- 2025年9月：25,000行（强素数定理，3周）
- 2026年2月：~200,000行（球堆积8维+24维，5天+2周）
每一次跳跃，产出的数量级增长一个台阶，但耗时保持在同一量级。
陶哲轩是Math Inc.唯一合作的AI公司。 对于这位可能是当世最伟大的数学家来说，选择只与一家商业公司合作，本身就是极强的信任信号。
Hack VC的投资理论博客用了一个极其精妙的类比：
“Cadence卖的是芯片设计的验证——一个所有芯片必须通过的门。Math Inc.要做AI生成软件时代的Cadence。”
在EDA（电子设计自动化）行业，芯片流片之前必须经过Cadence的验证工具签字。没有签字，就没有流片。Cadence因此嵌入到了整个半导体产业链的最底层——它的收入不是来自芯片本身，而是来自芯片不能被制造除非经过Cadence这一事实。
Math Inc.想做同样的事情：让形式化验证成为AI生成软件上线前的必经之门。
当然，这个类比有一个巨大的风险：芯片验证是强制的，软件验证不是。 Math Inc.赌的是——当AI生成越来越多的生产代码时，“验证”会从可选项变成必选项。
四、Axiom Math：24岁，Putnam满分，2亿美元
如果说Harmonic代表”技术架构派”，Math Inc.代表”长证明派”，那Axiom Math代表的是——“代码验证至上派”。
Carina Hong的故事像硅谷的剧本，但数据是真实的。
MIT本科期间发表了9篇数学论文（数论、组合、概率）。Putnam数学竞赛满分——过去100年，全球只有5个人拿过这个成绩。
23岁从斯坦福辍学。24岁拿到16亿。团队从Meta大量招聘，包括著名数论学家Ken Ono。
Axiom做的事情听起来很简单：用Lean训练AI，让它生成的每一个输出都经过形式化验证。
但为什么一个24岁的人值得$2亿？
因为Axiom已经做了两件大事。
第一件：Axiom的模型在Putnam竞赛上取得了满分。这不是比喻——是真正的数学竞赛满分。在过去的100年里，只有5个人类做到了这一点。
第二件：Axiom证明了一个20年未解的数论猜想——一个关于”沿曲面测量距离的微积分”的问题。这是Ken Ono本人多年来一直攻不下的问题。
Carina的”验证数据飞轮”理论是Axiom最核心的护城河：
“对于每一次AI输出，Axiom生成一个由大量经过证明检查的数据组成的’验证数据飞轮’。这些数据随后被反馈到训练循环中，以增强模型的能力——而不会引入未经验证的AI模型可能出现的’模型崩溃’。Axiom以此作为一个递归的自我改进循环。”
换句话说：Axiom的AI不仅会验证自己的输出，还会用验证过的输出重新训练自己。 这是一个不会”中毒”的自训练循环。
五、投资逻辑：为什么是现在？
把所有碎片拼在一起，AI for Math赛道的投资逻辑可以归纳为三点：
逻辑一：正确的时机
Jesse Han在IEEE Spectrum采访中说了一句非常精当的话：
“当我们创立Harmonic时，两样东西同时成熟了。Lean从beta软件变成了可以用于关键任务的Lean 4。GPT-4也开始展现出推理的曙光。我们只是第一个看到这两者可以结合的人。”
形式化验证工具 + 大语言模型 = 可验证的AI推理。 这个组合在2023年之前是不存在的。
逻辑二：唯一可以100%验证的AI
Vlad Tenev的核心洞察极其简洁：
“数学是唯一可以用编译器验证的智能。”
在其他所有领域——代码、法律、医学——AI的输出都需要人类判断对错。只有数学的Lean证明，可以被机器以100%的确定性验证。
这意味着：数学AI的训练信号是完美的。 没有模糊，没有标注噪声，没有”看起来对”。要么编译通过，要么不通过。
完美的训练信号 → 高效的强化学习 → 飞快的进步速度。
这就是为什么数学AI的进步速度（18个月从零到研究级）超越了历史上任何一个AI子领域。
逻辑三：通往通用AI的”最短路径”
Tudor Achim在多个场合说过同一句话：
“数学推理是所有定量科学的基础。解决数学推理，就解决了通往通用推理能力的核心瓶颈。”
这不是Marketing。如果一个AI可以证明范畴论中的同调代数定理（如Aristotle所示），那它距离”理解科学论文”就已经很近了。而”理解科学论文”距离”自主科学研究”——也许只是一步之遥。
六、中国：被低估的力量
最后必须谈谈中国的角色。
在这个赛道里，中国有一个显著的优势和一个显著的劣势。
优势：系统数量多。 DeepSeek、ByteDance、Tencent、Moonshot AI、BIGAI/北大……中国已经在AI数学推理领域部署了至少7个已发表系统，超过了全球任何其他国家。
劣势：学术影响力不够。 到目前为止，TongGeometry是唯一发表在Nature正牌期刊上的中国AI数学系统。中国的系统大多停留在arXiv预印本和基准测试上——能打，但”声音”不够大。
但有一件事值得特别关注：TongGeometry被ByteDance的Seed-Prover采用为几何推理模块。 这说明中国内部正在形成自己的”技术供应链”——学术研究（TongGeometry）→ 工业系统（Seed-Prover）。
如果这种模式在更多领域被复制，中国的优势将从”数量多”转向”质量高”。
这个赛道最有趣的地方不是”已经发生了什么”，而是”即将发生什么”。
Harmonic正在将Aristotle扩展到形式化代码验证。Math Inc.已经拿到了DARPA的国防合同。Axiom正在构建一个永不中毒的自训练循环。Theorem和Pramaana正在让形式化验证从”PhD手工活”变成”一键按钮”。
所有这些玩家都在赌同一件事：在一个AI生成越来越多软件、决策和知识的世界里，‘验证’将不是一种额外的质量检查——而是一种基础设施。
就像电力需要断路器。自来水需要水表。金融交易需要清算所。
AI输出需要形式化验证。
而这个基础设施层的市场——如果它真的形成——其规模可能超过今天任何人的想象。
因为软件比芯片多一百万倍。
“Cadence的伟大不在于它设计了芯片，而在于它让所有其他公司能够放心地设计芯片。Math Inc.、Harmonic和Axiom的野心是一样的——他们不想替代数学家，他们想让所有人放心地使用数学。这种基础设施生意，是硅谷最古老的致富公式。”
系列完结。
《AI for Math》五篇系列：
- AI是数学的孩子——从梯度下降到Transformer，算法的数学血脉
- 当AI开始做数学——从IMO银牌到研究级证明
- 陶哲轩的警告与预言——当证明多到人类消化不了
- 数学的反哺——下一个AI突破，可能藏在一篇无人问津的论文里
- 押注”数学超智能”——AI for Math赛道的公司、团队与资本地图