Carina Hong

Axiom 以 2亿美元 Series A、据报 16亿美元估值，押注的是正式数学成为基础设施，而不是停留在小众市场。 这家公司成立约 7至8个月，团队约 30人；它把数学视为自身 DNA，并把验证作为切入软件、硬件、科学和通用推理的第一个商业楔子。Hong 提出的 TAM 是“对所有 AI 生成代码拥有优先购买权”。

Hong 认为，验证的战略价值在于单位数据和算力带来更高智能，而不只是减少幻觉。 Axiom 的验证系统在 2025年12月 Putnam 考试中拿到 120/120；据报人类最高分为 110，MASS Arena 对比中 DeepSeek 得分为 103。她最具代表性的表述是“规模化聪明、复利式聪明”：证明把直觉转化为可复用、可协作的智力资本。

正式数据为 Axiom 提供了异常强的强化学习信号，但它的能力边界仍取决于底层 Lean 生态。 Lean 证明要么编译为正确，要么失败，因此可以在没有人工或 LLM 裁判的情况下进行递归拆解、回溯和验证奖励。但 Hong 承认，凡是 mathlib 缺少定义和基础设施的领域——尤其是微分拓扑和几何的部分方向——无论模型质量多高都依然困难。

单靠生成证明无法解决规格定义问题，Hong 将其称为经过验证的软件仍未解决的瓶颈。 证明可以确认代码满足形式化规格，但人类仍需判断这份规格是否真正描述了银行、飞控系统或用户想要的东西。“没有被规格化，就没有被证明”；因此，测试和 AI 生成的边界案例可能充当猜想，迭代改善规格。

硬件拥有最明确的近期付费意愿，因为“一个大部分经过验证的 GPU，也没有部分得分”。 节目提到，一些 ASIC 项目中，验证所需的团队规模和周期可能达到设计的 3至4倍；休闲定理证明中或许可以接受的随机重试，在这里不可接受。软件验证的覆盖面更广，但属于可选项，采用速度最终取决于验证的延迟、准确率和成本。

Axiom 押注 formal-first，但并非只做 formal。 Hong 表示：“我们不相信非正式数学系统会成为数学 AGI 的解决方案”，因为在前沿阶段，人工专家和 LLM 裁判的成本会高到无法承受。其目标引擎连接非正式直觉与正式证明；独立的数学发现系统则会在定理尚未准备好证明之前，先生成例子和构造。

长期护城河来自执行速度、专家密度和工作流控制权，而不只是专有证明。 Hong 认为积累的数据只是“时间护城河”，更重要的是数学家、Lean 贡献者、应用机器学习研究员和编译器专家之间形成的反馈回路。Axiom 免费提供约 14个 Lean 工具的套件 Axel，也在把公司定位为前沿实验室的验证伙伴：今天是“Claude 加 Axel”，未来可能是嵌入编码代理的一次 Axiom API 调用。

Hong 最宽泛的判断是，“经过验证的 AI 属于开放协作”，它可以通过共享、机器可检查的基础，支持人机协作，并最终支持代理之间协作。 她认为递归式自我改进无论如何都会发生；正式验证必须通过胜过替代方案来“赢得自己的位置”。整个领域的主要风险，是生态碎片化，以及在底层推理能力尚未成熟前，被迫证明短期商业价值。

🔗 原始收听与视频来源： 跨越非正式 AI 的规模化——Carina Hong、Axiom Math

Axiom押注6400万美元，认为可靠推理需要把生成与验证放进同一个自我改进闭环，而不只是训练一个更大的非形式化模型。 Hong 的架构由定理证明器、猜想生成器、共享知识库和自动形式化层组成，用 Lean 将概率搜索与确定性检查结合起来：「证明就是证明」（A proof is a proof）。

Axiom早期最强的技术信号，是在Putnam 2026考试时限内解出12道题中的8道，并在Hong首次发帖两小时后又报告解出第9道，最终得分仍待确认。 9道将追平前一年约4000名人类参赛者中的最高分，并大致达到Putnam Fellow水平；而「中位数分数基本就是0分」。Hong本人得了4道，还开玩笑说要办一场「击败Carina」派对。

商业切入口在验证劳动：硬件设计团队的规模可能只有验证团队的1/3或1/4，验证本身可能耗时3年；Hong认为AWS曾花5年时间，才把一个hypervisor内存隔离组件形式化。 Axiom瞄准芯片验证、安全关键代码审查、遗留代码等价性和数据库一致性——这些场景的客户「只希望它不要出错」。

Axiom并不认为每个程序都应该、或都能够进行形式化验证；Hong把市场分为关键系统、「有了更好」的场景，以及低风险的vibe-coded应用。 Lovable生成的网站「未必需要形式化验证」；她也承认「不可能验证Python里的所有代码」，但认为其中相当一部分仍可能覆盖。更难的产品问题，或许不是检查最终证明，而是在存在歧义时形式化正确的规格说明。

Hong预计数学不会消失，而是转向更高层次的抽象：顶尖研究者提供直觉，AI则成为「勤勉的研究生或博士后」，负责证明想法、构造例子并否定错误猜想。 Biewald追问机器最终可能超过人类直觉；她回答说会是「不同的直觉」，并认为要追上最顶尖的0.00001%数学家仍需很长时间。Axiom在P versus NP或黎曼猜想上「还没到那个阶段」。

这笔6400万美元融资，为一家成立约6个月、称自己「还在第0天」、仍与可信合作伙伴进行早期沟通的公司提供了发展空间。 Hong希望Axiom在面对大型现有企业时「始终保持不适」，保留她在地下中国摇滚乐队身上看到的、商业化之前那种「小而强悍」的饥饿感。技术里程碑很亮眼；接下来真正的考验是商业化，以及规格说明能否被用户真正使用。

🔗 原始收听与视频来源： 她筹集6400万美元，打造AI数学神童｜Axiom CEO Carina Hong