Axiom Math用AI代理将Stacks Project形式化验证为 1600 万行Lean代码
这家估值 16 亿美元的初创公司称，其AI代理团队已将约 7,654 页的Stacks Project翻译成约 1600 万行经计算机检查的Lean代码；CEO Carina Hong称这是目前形式化数学最大空白之一——代数几何——的填补。
AI解读：Axiom Math周三宣布已形式化验证Stacks Project，这是由人类撰写的最大的数学文献库之一。形式化指把证明改写成Lean代码，再由证明助手逐行检查逻辑是否成立。
据TechCrunch报道，Axiom的AI代理把该库约 7,654 页内容翻译成约 1600 万行计算机检查代码。难点在于Stacks中定理与定义相互依赖，团队必须在 1600 万行代码中保持每一条连接完整。
Axiom CEO Carina Hong表示，项目启动时团队并不确定能否做成，因为“大而精妙的东西在生活里就是不太搭”。技术团队成员Ashvin Swaminathan说，此前形式化数学中代数几何是一片“巨大黑洞”，现在研究者有了可依托的基础。
Axiom成立于 2025 年 3 月，Hong当时从斯坦福数学博士项目退学；公司在 3 月完成由Menlo Ventures领投的 2 亿美元A轮融资，报道给出的估值为 16 亿美元。
除数学家外，Axiom面向的还包括开发者：随着AI代理编写更多代码，验证代码无缺陷的难度上升，公司认为未来软件需要建立在已验证的基础之上。Swaminathan称这套Lean形式化是“代理可以在其上构建的基础层”。
Hong公开向所有编程公司发出挑战，要求它们在这一规模上做形式化。以上均为Axiom方面的说法与主张，来源未提供形式化质量的第三方评估或具体应用效果数据。
Axiom Math周三宣布，其AI代理团队已形式化验证Stacks Project——一个由数学家Johan de Jong于 2005 年发起、持续接受贡献的开源数学参考库。形式化指把数学证明改写为Lean编程语言代码，再由证明助手程序逐行检查逻辑是否成立。
据TechCrunch报道，Axiom的代理把该库约 7,654 页内容翻译成约 1600 万行经计算机检查的代码。Axiom成立于 2025 年 3 月，CEO Carina Hong从斯坦福数学博士项目退学后创办公司；公司在今年 3 月完成由Menlo Ventures领投的 2 亿美元A轮融资，报道给出的估值为 16 亿美元。
为什么Stacks难形式化
Stacks Project覆盖从大学代数到代数、几何与数论前沿的结果。与单一证明不同，库中定理和定义相互连接，每条结果都建立在更早的结果之上。Axiom团队必须在约 1600 万行Lean代码中保持这些连接完整。
Hong对TechCrunch说，项目开始时团队并不确定能否做成：“大而精妙的东西在生活里就是不太搭。”她说，Stacks是数学的基础性结果集合，定理之间需要一致、不能矛盾，定义之间也不能互相冲突。
Swaminathan说，已形式化的数学中代数几何长期是一片“巨大黑洞”，想在Lean中检查代数几何新工作的研究者此前缺少可依托的基础；他表示现在他们有了。
- Stacks Project：2005 年由Johan de Jong发起，开源、持续接受数学家贡献
- 覆盖范围：从大学代数到代数、几何与数论前沿
- 形式化产出：约 7,654 页对应约 1600 万行Lean代码
代理如何分工
Axiom给代理设定了松散的分层结构，让它们并行运行。Swaminathan说，这种分层并没有规定每个代理具体做什么，“代理自己在找任务，并识别出可以并行处理的事情”。
Hong说，公司还训练了自己的模型以擅长数学，她称多数其他验证类初创公司没有采取这一做法。起初团队依靠一名内部Lean专家教代理“人的品味”，后来她说代理已能自行形成判断。
Hong认为，代理在构建Stacks时采用的并行、自选任务方式，也会是未来AI工作的重要形态：代理需要一个可复用的知识库作为基础，否则早期糟糕的工程选择会让后续扩展变得困难。
目标不止于数学
Swaminathan说，Axiom相信数学是构建这类验证基础的起点，而且这种能力可以迁移。他称这套Lean形式化现在是“代理可以在其上构建的基础层”，代理能读取并理解这些代码，再在其上搭建新设施。
对开发者而言，Axiom的主张指向代码正确性与安全漏洞的保证问题；随着AI代理编写更多代码，这一问题会扩大。报道未给出Axiom技术用于软件验证的具体案例或效果数据。
Hong公开向所有编程公司发出挑战，要求它们在这一规模上做形式化。这一挑战以及Axiom对自身工作的定位，目前均为公司方面的说法。