她筹集6400万美元，打造AI数学神童｜Axiom CEO Carina Hong
摘要
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在面对大型现有企业时「始终保持不适」，保留她在地下中国摇滚乐队身上看到的、商业化之前那种「小而强悍」的饥饿感。技术里程碑很亮眼；接下来真正的考验是商业化，以及规格说明能否被用户真正使用。
精读
上游暂未提供，后续同步将继续补齐。