跨越非正式 AI 的规模化——Carina Hong、Axiom Math

摘要

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

精读

1. 正式数学是 Axiom 切入横向市场的楔子

• 这轮融资体现了其主张的规模：Axiom 成立仅 7至8个月、团队约 30人，却以据报 16亿美元估值融资 2亿美元。一位主持人将其与美国数学研究据报每年 2.5亿美元的预算相比较；Hong 回应“好吧，哇”，主持人说“我们应该在数学研究上投入更多”，Hong 则称这种情况“有点悲哀”。

• Hong 的类比对象是 2024年前后的编程：竞争对手把编程视为一个 B2B 垂直领域，Anthropic 则把它当作能够迁移到更广泛推理能力的结构化训练数据。Axiom 认为，正式数学也有同样的因果路径——先处理结构化、可验证的工作，再形成远超表面垂直领域的能力。

• 公司的“DNA 仍然是数学”，使命是打造超越人类的数学家，但 Series A 让它得以“拓宽我们的梦想”。正式解决数学问题是最好的第一市场，因为它既能训练通用推理引擎，又能产出适用于代码和硬件的技术。

2. 验证的目标应是让聪明复利，而不是监管错误

• Hong 拒绝沿袭地铁信号切换、航天器、飞机和企业系统留下的合规时代叙事：在那种叙事中，形式化验证是为防范边界情况而支付的昂贵税费。她将其反转为：“对我来说，验证不是关于损耗。对我来说，验证是规模化聪明、复利式聪明。”

• Ramanujan 是她最核心的类比。他的直觉已经产生了非凡公式，但在 Hardy 和 Littlewood 的帮助下学习写证明后，这些直觉才变成后来数学家可以信任、扩展的定理：验证让聪明“向上规模化，也向外扩展”。

• Lean 通过 Curry–Howard 对应提供机器可检查的基础，把证明转化为程序。它既是函数式、图灵完备的编程语言，也是证明语言；在不使用 sorry 等不安全捷径或自行发明公理的前提下，编译通过的证明就是真正正确的。

• 甚至在 AI 出现之前，Lean 的 grind 等 tactic 就已经能够处理低层推导，让数学家留在高层直觉空间。这也回答了 Hong 自己关于数学家为何需要证明助手的问题：人工同行评审可能耗时 2年，而工具既能验证，也能扩展研究者可以尝试的范围。

3. 经过验证的生成已经带来性能提升

• Hong 将 2025年12月 Putnam 视为正式系统与非正式 LLM 的首次决定性比较。MASS Arena 据报给最高分 LLM DeepSeek 打出 103/120，人类最高分为 110；最高分学生身份未知，据报可能来自 MIT 或 Chicago。Axiom 实时参赛并拿到 120/120。

• 这一结果的重要性在于，Axiom 使用的数据量比前沿规模的非正式系统少了“几个数量级”。Lean 数据提供二元基础，因此模型可以针对正确性已知的证明进行强化学习和微调，而不必依赖偏好模型对正确性的估计。

• Axiom Prover 并不是一个 LLM，而是一组经过后训练的模型加工具。Hong 表示，推理能力仍可通过把证明目标递归拆成子目标，以及学习回溯来扩展；截至目前，尚未观察到迫使收益停止的“几乎任何上限”。

4. mathlib 的覆盖范围定义前沿，数学发现需要另一套引擎

• 主持人直接提出了分布偏移问题：递归 rollout 可能会在原始训练领域周围形成崎岖的能力前沿。Hong 承认，问题首先是基础设施——如果 mathlib 没有某个领域所需的定义，系统就没有坚实基础可用，无论其通用推理能力多强都一样。

• 她将相对容易编码的代数，与涉及收敛和极限的分析及相关定义作了对比。因此，Axiom 预计自己在微分拓扑、微分几何等形式化稀疏的领域表现更弱；同时，公司称已在数论、交换代数、代数几何、离散数学、组合数学和概率领域取得研究成果。

• 组合数学仍然异常困难，因为决定性构造可能高度依赖创造力。Hong 指出，AlphaProof 在 2024年 IMO 中取得 28/42，并认为 2025年表面上跃升至 35分，主要是因为当年只有一道组合题；系统此前已经能够解决非组合题。

• 因此，Axiom 正在开源两套面向猜想形成前阶段的数学发现代码库。这些工具搜索数列、图、反例和其他构造，为直觉提供素材，然后再交给 Axiom Prover 处理引理；Hong 强调，“数学不只是证明”。

5. 经过验证的代码必须拆成可分解的组件生成

• 当主持人提到 Rice 定理、可判定性和不完备性时，Hong 接受了理论边界：不是每个程序都能被形式化验证。她的实际回答是，理论上的不可能并不妨碍验证“绝大多数有用程序”。

• 设想中的编码工作流，是把分布式系统或其他复杂任务持续拆解，直到某个组件既重要到必须确保无误，又足够小到可以验证。此时 Axiom 可以作为现有代码的验证伙伴，也可以作为生成器，同时产出程序及其证明。

• 主持人用 Lean 作了类比：更高层是否可以暂时通过 sorry 假设某个组件？Hong 表示，这在数学中相当于一个尚未证明的引理，但并不是目标中的编码架构；Axiom 希望每个已规格化的组件都带着支撑其保证的底层证明交付。

• Hong 的愿景表述是：“凡是能够定义的，都能够执行；凡是能够规格化的，都能够证明。”但她立即称这部分是营销语言，并补充“基本上”“希望如此”。设想中的映射，是从程序加陈述，转化为验证条件加证明。

6. 规格定义，而不是证明检查，是尚未解决的信任边界

• 主持人反复追问语义是否对齐：一个很小的 Lean 对象可能内部有效，却没有证明人类以为它证明的内容。Hong 的回答仍然要求检查形式化验证条件是否忠实表达了原始编码问题；检查器可以消除证明错误，却不能消除意图错误。

• 飞控和银行审计的例子暴露了这一缺口。人类并不擅长陈述所有想要的行为，例外情况也会被遗漏，而“没有被规格化，就没有被证明”。当被问到什么能解决这个问题时，Hong 坦率回答：“我们还没走到那里。”

• 她认为测试是互补手段，而不是已经过时。基于变异的单元测试生成，以及 AI 追问“你考虑过这个情况吗”，都可以提出规格中遗漏的部分；在她的类比里，测试承担猜想形成的角色，证明器则负责最终证明。

• 自动形式化尤其困难，因为英语问题必须先变成形式化陈述，之后才有可能求解。输入输出测试案例可以为编码规格提供基础，但数学陈述往往没有数值答案；其形式化仍需要人类“扫一眼”，确认原本想表达的主张在转译后没有变形。

7. 更大的证明树把瓶颈从正确性推向注意力

• Hong 估计，当前经过验证的软件可能平均每 1行代码需要约 20行证明，并承认“我没有一个关于这个规模定律的好答案”。不过，Axiom Prover 已经从处理约 40个节点的证明树，进展到约 4,000个节点；在基础模型或上下文限制成为主导瓶颈前，她认为仍有很大提升空间。

• 假设存在一份证明 Riemann 假设的百万行 Lean 证明——明确只是一个假设——它可以是正确的，却很难理解。Hong 预计，人类仍会通过非正式摘要和往返一致性检查来寻找解释；而“注意力才是瓶颈”，品味则决定哪些结果和替代证明值得分配稀缺的人类及算力资源。

8. 硬件带来紧迫性，软件带来可选性

• Hong 将软件的广阔机会定义为“对所有 AI 生成代码拥有优先购买权”：每个工作流都可以在验证价值超过成本时选择验证。这一市场远大于传统上受监管或安全关键客户的集合。

• 硬件是必须覆盖的滩头阵地，因为“一个大部分经过验证的 GPU，也没有部分得分”。主持人提到，设计与验证在团队规模和周期上的比例约为 1:3 或 1:4；Hong 补充说，单个逻辑验证问题就可能消耗数百人和数千个工具许可证。

• 当有人出于娱乐目的“抓宝可梦”式地反复生成数学问题时，随机生成或许可以接受，但这无法满足完美证明器对硬件的要求。一个声称成立的证明，要么每次都验证电路保证，要么整个工作流就失去意义。

• 软件处于连续谱上：侄子的 Lovable 网站不需要形式化证明，而受监管的企业代理可能需要。即便是潜在危险的代理行动，有时也可以通过限制行动空间，以更低成本加以约束；因此 Hong 表示，最终采用与否取决于验证能否足够快速、准确、便利，真正成为一种可选项。

9. 面对无限算力质疑，Axiom 的 formal-first 信念仍然成立

• Hong 以绝对措辞提出论点：“我们不相信非正式数学系统会成为数学 AGI 的解决方案。”主持人的反驳是，只要强化学习资源足够、前沿实验室投入足够，系统或许永远不会耗尽燃料；Hong 则补充说，无限资源按定义可以避开限制，但现实系统要面对经济性和稀缺的专家判断。

• 非正式前沿数学需要人工评分者或 LLM 裁判，而能够评估 Langlands 纲领等领域非平凡工作的专家，不可能无限规模地供应。Hong 认为，当评判成本压垮能力收益时，“不可能”和“极其昂贵”在运营层面就趋于一致。

• 这场押注并不是要抛弃非正式推理。非正式与正式结合的引擎，可以用语言处理直觉和规划，同时由 Lean 提供有基础的奖励；Hong 预计，正是把证明转化为程序，才能改变样本效率曲线。

10. 来源追溯失败说明，证明与新颖性是两类不同问题

• Hong 回顾了 Axiom 围绕 Erdős 问题 124 和 481 的错误主张。这家年轻公司相信了竞争对手 Harmonic 的文献审查，尝试解决据称尚未解决的问题并发现了证明，后来却发现两家公司都错了，因为这些问题早已被解决。“我们确实应该做好自己的工作。”

• “Dead Ends in Square-Free Walks”也出现了类似问题：一个早先的答案最终被追溯到网上的一篇帖子。搜索之所以困难，是因为一个结果可能以不同语言出现，也可能只是另一条定理近乎显然的延伸；机器验证无法确认历史新颖性或来源。

• 她由此得出的教训是，知识图谱或知识库应当成为任何公司的重要组成部分，而且“没有得到足够讨论”。Erdős 事件之后，Axiom 对声称发现新解更加谨慎，将证明有效性与检索、归因和新颖性审查分开。

11. 运营护城河是跨学科反馈回路

• Hong 将 Axiom 的速度归因于研究型数学家和奥数数学家、mathlib 贡献者与 Lean 专家、来自大型实验室的应用机器学习研究员，以及代码生成或编译器专家的组合。数学家本身也是用户，因此迭代回路“极其快速”。

• 她拒绝使用永久护城河的说法：专有合成证明和累积数据只构成一条“时间护城河”，是通过更快执行获得的临时缓冲。竞争对手可以收集类似数据，因此优势必须依靠能力提升、工具和人才密度不断更新。

• 她自己的经历也体现了这种混合路径。Oxford 的神经科学本科阶段让她了解“什么是困难的”，同时接触到 AI 研究；法学院则让她看到许多系统的规格定义都不完整。她开始数学博士学习后几乎立刻就开始融资，因为她已经“疯狂地爱上了 AI 将要做数学这个想法”。

• 一名前 Facebook 产品负责人给出的建议让她最终做出决定：比较时间实际流向哪里，然后“跟随你的能量”。Hong 的分配结果是“100%、0%”地倒向创业想法；她认为这必须是一家营利公司，因为机会远远超出数学突破本身。

12. Axel 把 Lean 基础设施变成协作层

• Axiom 发布了 Axel——Axiom Lean Engine——一套免费、约 14个工具组成的 Lean 原生验证、操作和修复工具。其 Verified Proof 组件会检查不安全公理及其他作弊方式；Hong 表示，其中一条验证路径的速度约为对比工具的 100倍，而修复工具的目标，是成为现有基于 LLM 的修复方法更便宜、更直接的替代方案。

• 据报，早期用户将“Claude 加 Axel”组合使用，把它应用于区块链工作，也在形式化一个与 Donald Knuth 相关的 Ramsey 结果时使用了它；Hong 对报道本身及具体结果都保留了余地。她对前沿实验室的合作提议很明确：实验室应继续强化代码生成能力，并像调用专业搜索 API 一样，在验证环节调用 Axiom。

• Axel 在 Axiom 参加 Putnam 考试时也属于必需工具：团队在周六的“战情室”里对照官方试卷工作；Hong 表示，如果没有这些工具，解出 8道题也无法在规定时间内完成。同一套验证器还可以成为针对 Lean 程序进行强化学习时的精确奖励。

• 共享工具可以让数学更具协作性，但 Hong 表示，人类生成的蓝图仍然至关重要。大型形式化项目会把定理拆成子问题，但 Terence Tao 等专家仍然决定这些部分如何拼接；自动生成这类蓝图，是一个重大的技术瓶颈。

13. 经过验证的 AI 必须靠执行赢得自己的位置

• Hong 最后的哲学反转是：“经过验证的 AI 属于开放协作”，而不只是属于规则繁重的封闭行业。Lean 已经为人类之间协作制定蓝图提供了基础；同一形式层也可以支持人机协作，并最终支持代理之间协作，而不要求参与者彼此盲目信任。

• 她将 Axiom 定位在基础设施栈上：数学可以间接解锁科学，但形式化推理也能直接迁移，因为代码连接了非正式语言与严格符号结构。系统的目标，是把高层直觉与低层保证连接起来，而不是在二者之间二选一。

• Hong 表示，递归式自我改进“无论如何都会发生”；Axiom 的任务，是让正式验证足够好，从而被接纳进这一循环。“当你把这个问题归结为执行问题时，就应该直接去做。”

• 她对整个生态最大的担忧是碎片化：充裕资本可能鼓励优秀研究者各自创办孤立公司，花数月时间做交易，在任何一个类别证明自身存在价值前就稀释团队。对于数学 AI，商业验证点和 4个月目标有帮助，但如果它们分散了对长期核心能力的投入，反而可能成为更深层的瓶颈。