0｜基本信息（Metadata）

  • 受访者：Carina Hong（洪乐童），2001 年生于广州，Axiom 创始人兼 CEO
  • 采访者 / 媒体：张小珺（Xiaojun），”张小珺播客”（Xiaojun’s Podcast）
  • 采访地点：美国硅谷，Facebook 创业起步的小蓝屋（Facebook House）
  • 采访时间：2026 年 4 月（视频发布于 2026-04-19），全长约 4 小时
  • 采访背景：Carina Hong 创办的 Axiom（AI for Math 方向）刚完成 Series A 融资，估值 16 亿美元。触发公众关注的导火索是”57 岁美国终身教授辞职去给 24 岁中国女孩打工”的新闻。本次采访发生在 AxiomProver 在 Putman 数学竞赛获得 98 年历史中第 6 个满分之后，是硅谷 Neo lab 生态中最新鲜、最完整的一次创始人深访。

Carina Hong 的背景高度跨界：MIT 数学+物理本科 → 牛津罗德奖学金（神经科学硕士）→ 斯坦福数学+法学博士（退学创业）。自认”暴力计算型数学家”，非天才型。她的身份定位是”学徒”（Apprentice），墓志铭只写这一个词。

1｜核心观点（Core Views）

观点一：AI for Math 的核心不是模型，而是系统（system）

Carina 反复强调 Axiom 不是一家”模型公司”，而是一家”深科技公司”（deep tech company）。她押注的是 orchestrator + subagents 架构 + 形式化验证工具链，而不是堆算力、堆参数。她认为——模型会被 commoditize（DeepSeek 已证明这一点），但系统层面的工程能力才是真正壁垒。她用了 SpaceX 的类比：火箭（系统）能上天，不是因为发动机比别人多一个，而是整个系统设计对了。

可信度判断：这是目前 Axiom 最清晰的差异化叙事，逻辑自洽。尤其在 DeepSeek 把模型价格打下来之后，”不是模型公司”成为有说服力的定位。但系统壁垒最终需要产品落地来验证。

观点二：数学是真实世界的沙盒（sandbox），AI for Math 将从数学扇形展开到芯片验证、代码验证

Carina 认为数学提供了 最干净的人造世界——验证信号明确（证明对就是对，错就是错）、描述规范、数据结构化。这意味着：AI for Math 的技术可以直接迁移到芯片验证、代码验证、物理仿真等 B2B 市场。她称 Axiom 的业务模型为”扇形展开”（fan-shaped），从数学这个圆心向外辐射。

可信度判断：Amazon 的实例（3-5 年手写 26 万行 Lean 代码验证一个 CPU 内存隔离组件）直接展示了市场需求。问题在于：从 Putman 满分到工业级代码验证之间，距离有多大？Axiom 尚未展示这方面的产品化进度。

观点三：Axiom 在做 ASI（Specialized Super Intelligence），不是 AGI

这是一个激进的定位声明。Carina 认为超级智能应该是专业化的，而不是通用的——”我永远不会去拿诺贝尔文学奖”。数学形式化验证和编程验证是同一个光谱的两端，Axiom 将专注这个光谱。

可信度判断：这与其说是技术判断，不如说是战略定位——避免与 OpenAI/DeepMind 在通用领域正面竞争。此叙事对投资人有利（差异化+可落地），但”ASI”的概念仍是营销层面的包装，离真正的”超级智能”还有距离。

观点四：真正的数学家在AI时代不会消失，角色将从”解题者”变为”问题筛选者”

Carina 引用 Jevons 悖论——工具越高效，使用越多。她认为 AI 证明不会减少数学家的需求，反而会增加：数学家将提供 0.01% 的直觉，决定算力该集中在哪些问题上。她同时强调数学家社区的文化价值（生日峰会、合作传统）不可被 AI 替代。

可信度判断：这是一个对数学家群体友好的叙事，也符合历史经验（计算器没有消灭会计）。但”0.01% 直觉分配算力”的理想化程度较高，实际中可能遇到”少数人垄断算力分配权”的问题。

观点五：”我是个学徒”——创始人身份在”不想当CEO”中演化

Carina 多次坦言”从来没想创业”、”最快乐的状态是做实习科学家”。CEO 身份是团队推动的副产品。她的领导力哲学是服务型领导——”不是前面拿喇叭的人，是后面发水的那个”。她自创”企业家三分类”：visionary（远见型）、execution（执行型）、sales（销售型），自认是 visionary。

可信度判断：非常真诚。00 后、女性、非典型硅谷创始人，这套叙事既是真实的认知，也是一种有效的领导力工具——刻意淡化权力以维护自下而上的文化。但”不想当CEO”和”登月使命”之间存在内在张力，公司进入成长期后这种 tension 可能加剧。

2｜话题分析（Topic Breakdown）

话题一：Axiom 的技术路线——为什么选 Putman 而非 IMO

AxiomProver 在 2025 年 12 月的 Putman 数学竞赛中获得满分（98 年历史中第 6 个满分，前 5 个是人类）。与 DeepMind AlphaProof（2024 IMO 银牌）的差异：

  • 核心信息：Axiom 选择 Putman 而非 IMO，因为 Putman 的题目需要更复杂的推理链（非固定解题套路）。但 Carina 也坦言 Axiom 没有参与”First Proof”挑战不是因为能力不足，而是那些题在 Lean 库里根本没有对应的定义——”我连题目都放不进去”。
  • 关键细节：Putman 现场 Ken Ono 说 “It’s a state of war now!”；Axiom 4 个月拿到满分，而竞争对手花 2 年解出 IMO 6 题中的 5 题。
  • 值得注意：对 DeepMind 的态度微妙——尊重（”跨世纪时刻”）但立刻强调 Axiom 的突破在”研究级数学”层面而非奥数层面。这是有意识的技术定位竞争。

话题二：Axiom 的人才磁铁——从”读论文”到”作者加入团队”

  • 核心信息：Axiom 的关键成员包括 Ken Ono（美国数论学家，第15号员工）、Shubho Sengupta（CTO，CUDA 早期开发者、Baidu Mafia）、François Charton（Mistral 首席科学家合作者，2019 年”Transformer 能做微积分”论文作者）、Bartosz Piotrowski、Evan Chen（美国 IMO 教练）、Kenny Lau（Lean 生态核心贡献者）。
  • 关键细节：Carina 提到 AI for Math 前 30 篇论文中，”大部分作者的作者现在都在 Axiom”；她把与 Shubho 的相识描述为 Verve 咖啡店长达一年半的”无目的闲聊”；对人才不”销售”而”展示”——”我不能说服你，我只能说服我自己”。
  • 值得注意：招聘策略不存在，更像引力场（”两条鲸鱼找到彼此”）。这种叙事很浪漫，但也隐含风险——依赖创始人的个人磁力而非组织流程。

话题三：自动形式化（Auto-formalization）——最难的技术瓶颈

  • 核心信息：Carina 认为把 arXiv PDF 转化为 Lean 代码比自动证明更难，但获得赞誉更少。20 页论文 → 200-500 页 Blueprint → Lean 代码。Lean 全球总量 tokens 极少，使得这个转换极其困难。
  • 关键细节：所谓”定义缺失”（missing definitions）是当前最大的天花板——很多数学概念在 Lean 库里没有定义，导致连题目都无法形式化。
  • 值得注意：这是这个采访中最诚实的自我评估之一。承认最大的瓶颈在自己手上，而不是竞争对手。

话题四：竞争格局与资本市场认知鸿沟

  • 核心信息：Carina 称 AI for Math 领域只有两家公司（Axiom + 一家竞品），”不是蓝海，很困难”。”模型 commodities 化”之后，VC 对”AI 公司”标签极度敏感，认为 Axiom 只是又一个 AI 模型公司，”投资人觉得我疯了”。
  • 关键细节：种子轮估值 $3 亿（6400 万融资），A 轮 $16 亿。竞争对手早两年起步、融资 5 倍、估值 5 倍。
  • 值得注意：Carina 对”年轻做 deep tech 是减分”的观点直言不讳，同时声称”作为华人女性既不加分也不减分”——可能低估了身份因素的实际影响。

话题五：Neo lab 运动与”登月科学”

  • 核心信息：Carina 的创业哲学深受 Peter Thiel（”垄断带来创新，竞争带来平庸”）和 Neo lab 运动的影响。她经常引用 SpaceX 类比——要么登月成功，要么火箭爆炸，没有中间状态。
  • 关键细节：公司成立仅 7 个月就完成 A 轮融资；团队从 15 人（Dec 2024）增长到 30 人（采访当时）；工作节奏”996”被提及作为行业状态。
  • 值得注意：”执行速度让我学习的时间越来越少”——做深科技的人必须同时是 CEO 和研究者，这个矛盾可能是 Axiom 最大的生存风险。

3｜关键数据与预测（Key Data & Predictions）

内容 数值 / 时间节点 来源可信度
Axiom 种子轮估值 3 亿美元（融资 6400 万） 高
Axiom A 轮估值 16 亿美元 高
Putman 竞赛满分 2025 年 12 月 6 日，98 年来第 6 个满分 高
AxiomProver Putman 成绩 12 题全部解出，下午 3:58 达 8 题 80 分（世界前 5-20） 高
DeepSeek 发布冲击 2024 年 2 月 → 市场对模型公司极度谨慎 高
AlphaProof IMO 2024 成绩 28 分（银牌，差 1 分金牌） 高
Amazon 形式化验证工程 3-5 年，26 万行 Lean 代码，验证一个 CPU 内存隔离组件 中（二手信息）
团队规模 2024/12：15 人 → 采访时：30 人 高
竞争对手规模 约 50-75 人 中（推测）
DeepSeek-Prover Putman 宣称成绩 49/600+ 题，实际 47 题（2 题作弊） 高（Carina 陈述）
Axiom 自建验证器性能 比社区版快 100 倍 中（技术自评）
AI for Math 前 30 篇论文作者 “大部分在 Axiom” 中

预测性判断：

  • 2026 年将出现 AI for Math 的 “ChatGPT moment”（Carina 认为 Putman 满分是她的 “AlphaGo moment”）
  • 传统 SaaS 会死，forward deployment 是未充分创新的方向
  • 持续学习的小模型、好的多模态模型、Agent 经济学将在 2026 年由 Neo lab 类小公司推动
  • 数学验证与代码生成将合二为一——”anything you can define, you can prove”
  • 芯片验证将是最早的 B2B 落地场景

4｜逻辑与依据评估（Logic & Evidence）

整体逻辑强度：中 → 强

价值：

  1. 内部一致性高：从”我是暴力计算型数学家”到”AI 最能帮助暴力计算型的数学家”到”Axiom 做暴力搜索系统”，叙事弧高度自洽
  2. 技术路线清晰：知道瓶颈在哪里（自动形式化、定义缺失、library learning），也知道下一步做什么（猜想的奖励信号、持续学习）
  3. 竞争分析务实：直承”不是蓝海”、”市场很困难”、”投资人觉得我疯了”，没有过度乐观
  4. 自我认知成熟：知道”执行速度 vs 学习时间”的矛盾、知道年轻做 deep tech 是减分

折扣因素：

  1. 缺少可验证的产品指标：除了 Putman 分数和 Verina benchmark，没有展示产品化的追踪记录
  2. 架构细节空缺：说到 library learning 时说”社区卡住了”，但未说明 Axiom 自己的解法
  3. 商业化路径仍模糊：芯片验证的逻辑链条成立，但没有时间线、客户名字、收入数字
  4. “双寡头”格局叙述：声称只有两家公司在这个领域，但忽略了 Google DeepMind、OpenAI 等巨头随时可能加大投入
  5. 失败的归因偏向乐观：说”失败了就去做数学家/神经科学”——暗示可以承受，但 16 亿估值的 A 轮压力不会这么轻松

5｜弦外之音（Reading Between the Lines）

1. 刻意回避：预训练的具体路线

当被问及是否做预训练时，Carina 先闪烁其词（”可能涉及其他公司的秘密”），然后说”太贵了不做”。这可能意味着：

  • Axiom 在预训练方向上有关注但资源不足
  • 存在非公开的合作关系不能透露
  • 或者确实已经决定走后训练路线，但这个回答的措辞比预期更谨慎

2. 措辞值得注意：”我不太喜欢 AGI 这个词”

Carina 在好几个地方与主流 AGI 叙事保持距离。用 ASI（Specialized Super Intelligence）替代 AGI，用”登月科学”替代”改变世界”。这可能意味着她有意在价值观上与 OpenAI 为代表的”AGI 狂热”划清界限，定位更接近 Elon Musk 式的”硬核工程浪漫主义”（”SpaceX 火箭要么上天要么爆炸”），而不是 Sam Altman 式的”全球通用智能共同体”叙事。

3. 对华人身份的边界保持

“作为华人女性既不加分也不减分”——这个表述本身就很谨慎。结合她母亲是北京人、广州成长、全英文接受教育、在硅谷创业的背景，这可能反映出她对族裔政治话题的回避策略：不在此处做文章，让别人用结果说话。

4. 对 DeepSeek 的微妙点评

先给予极高尊重，然后点出 Putman 作弊事件（2 题用奇怪公理作弊），最后补一句”最关键的东西不会写在论文里”。这可能意味着：

  • 她知道中国 AI community 的开放性和学术诚信水平
  • 也在暗示 Axiom 有一些不能公开的核心技术
  • 客观上也传递了对中国 AI 公司的警惕性尊重

5. 未说出口的焦虑

反复出现”99% startup 会死”、”执行速度 vs 学习时间”、”我什么都不知道”等措辞，暴露出创始人阶段的真实压力。但每次焦虑出现后，Carina 会用”登月使命”或”学徒身份”的叙事迅速对冲——这可能是一种已内化的心理保护机制。

6. 关于数学直觉与古典工具的圈层信号

提到 Oxford 的 Roger Heath-Brown 生日峰会、Ben Green、James Maynard、Hardy-Littlewood 圆法、筛法——这些信号（而非商业术语）是她的真实身份标识。这可能意味着：

  • 她终究在灵魂深处是一个数学家，而不是一个 CEO
  • Axiom 的产品最终可能会服务数学家社区优先于商业客户
  • 对 “classical analysis” 的强调暗示了 Axiom 技术路线上的某种学术保守性

6｜可操作信息（Actionable Takeaways）

  1. AI for Math 赛道的投资窗口已接近关闭 — Carina 直言”只有两家公司”，新入局者”会跟我们两年前一样”。如果对这个赛道感兴趣，参与 Axiom 或竞品的后续融资比从零起步更务实。

  2. 形式化验证在芯片验证领域有明确商业需求 — Amazon 的 26 万行 Lean 代码案例是强有力的市场信号。任何做 EDA（电子设计自动化）或芯片验证的公司应该关注 Axiom 的产品化进度。

  3. “自动形式化”（Auto-formalization）是下一代 AI 基础设施的关键技术 — 比自动证明更难，但却被低估。从现在开始积累 arXiv PDF → 形式化代码的技术储备，可能在三到五年内成为核心竞争力。

  4. “持续学习小模型 + Agent 多模型协作”的架构范式值得关注 — Carina 明确押注系统而非单一模型，认为 orchestrator + subagents + 形式化验证工具（作为 RL reward）是下一代方向。这与当前”更大 LLM”的主流方向形成有趣的对照，值得技术投资人留意。

  5. Neo lab 运动正在硅谷崛起 — 登月科学、反主流竞争文化、技术专家治企（Technocracy）的价值取向正在凝聚。这是一个值得追踪的硅谷意识形态谱系变化。

7｜一句话总结（One-line Summary）

24 岁华人女孩的 Axiom 在 Putman 上碾压人类之后，正试图用形式化验证重构”AI 时代数学研究”的定义——但真正的战场不在 IMO 或 Putman，而在芯片验证等 B2B 市场的落地能力。