发生了什么
- 估值16亿美元的初创公司Axiom Math于2026年11月4日（星期三）宣布，已对Stacks Project完成形式化验证。TechCrunch于11月5日报道了此事。
- Stacks Project是一个开放的参考文献，由哥伦比亚大学数学家Johan de Jong于2005年发起。它汇集了代数、几何和数论方面的成果，从大学水平一直到该领域的高深课题。
- Axiom的AI智能体集群把其约7654页的内容翻译成了约1600万行Lean代码；Lean是一种语言，在其中，一个叫作证明助手的程序会逐行检查每一个证明。
- 这些智能体在宽松的结构下并行运行。据Axiom的Ashvin Swaminathan说，存在一个层级，但智能体会自己找出可以同时处理的任务。
为什么重要
- 如果一个证明通过了证明助手，就可以相信它在逻辑上是可靠的。这是检验数学的另一种方式，不同于同行阅读。
- 这一成果针对的是一个已知的缺口。Swaminathan对TechCrunch说，已形式化的内容中存在“这样一个巨大的黑洞”，它涵盖了代数几何。
- 公司看到了数学之外的用途：一个经过验证的基础，智能体可以在其上编写缺陷和安全漏洞更少的软件。
关键数字
1600万行。 这是Lean代码的大致规模。难点不仅在于每一条定理，还在于让相互依赖的定义与结果之间的联系保持完整。
背景
Axiom由Carina Hong于2025年3月创立，她今年25岁，离开了斯坦福大学的数学博士项目。今年3月，公司完成了由Menlo Ventures领投的2亿美元A轮融资。Hong对TechCrunch说，团队当时不确定用智能体编写代码能否保留Stacks的结构，而且定义之间不能相互矛盾。
该公司还训练了自己的数学模型。起初，由一位内部的Lean专家教它们判断力；据Hong说，随着时间推移，它们自己学会了。这是公司的说法，在TechCrunch的这篇报道里无法与外部评审相核对。
在相关话题上，Mamífero 还发布过：Claude用形式化验证测试了123个开源库的安全性；ThinkingBox奖励智能体留下的数据库；Recursive发布Flint，一个面向笔记本电脑的编程模型；GitHub Copilot新增了包含多个智能体的项目。
接下来
- 代数几何研究人员将有材料，可在Lean中检验自己的新成果；据Axiom说，这在以前几乎不存在。
- 每一个经过验证的结果，都是未来证明的一块积木，这样就没有人需要从零开始。
- 外部的数学家尚需判断，这种翻译对他们的日常工作有多大用处。
一句话总结
一部由人们花二十年写成的文库，如今也有了机器可以检验的代码形式。它的价值，要看有多少新的证明建立在它之上。
来源
- TechCrunch，“Axiom Math wants to keep AI slop out of mathematics”，2026年11月5日，链接。
- 封面图片：Tungsten，公有领域，来自 Wikimedia Commons
编辑：Rodrigo Cornejo。我们如何挑选和核实：谁在写这些笔记。