**Carina Hong，Axiom Math 创始人兼 CEO，在公司完成 2 亿美元 A 轮融资后**，做客 AI for Science 播客，核心论点是：通往超级智能的道路必须通过形式化验证（formal verification），而不是把它当成修 bug 的工具。她认为，只有形式化方法才能让 AI 的「聪明」被可靠地累积和规模化。Axiom Math 成立仅 7 个月、团队 30 人，就在 2024 年 Putnam 竞赛中拿下满分 120/120，击败了当时所有人类和 AI 系统。

**[Carina] 明确反对当前主流的大语言模型「纯靠更多数据和算力堆出数学能力」的路径。** 她指出，非形式化的 RL（如基于 LLM 判别的奖励信号）存在严重的稀疏性和噪声问题，而 Lean 定理证明器结合强化学习能提供 **「稠密且可验证的训练信号」** ——每一次推导要么被 Lean 检查通过，要么不通过，没有模糊地带。她预测，未来 3-5 年内，**任何严肃的数学 AI 系统都必须内置形式化验证引擎**，否则无法实现可靠的自我改进循环。她同时批评了「让模型在 ProofNet 这类非形式化数据集上 Fine-tune 就能做好数学」的观点，认为那只是模式匹配，不是真正理解。

**一个值得持续关注的判断：数学 AGI 不可能由纯非形式化系统实现。** Carina 认为，**「规范难题」（specification problem）** 是无人问津却最关键的瓶颈——人类目前难以写出完美精确的数学问题形式化描述。什么算是「已解决」？什么步骤可以省略？这些都需要形式化框架来界定。另外，Axiom Math 计划开源其 Lean 数据基础设施 **Axle API**，这可能成为数学 AI 领域类似 vLLM 之于推理基础设施的通用层，值得长期跟踪其生态效应。