AxiomMath 借助 AI agents 形式化验证 Stacks Project

AxiomMath 已将 Stacks Project 的约 7,654 页数学内容转化为约 16 million 行经计算机检查的 Lean 代码。公司让 AI agents 自行寻找任务并并行处理，以保持约 16 million 行代码中定理、定义及其依赖关系的一致性；这项工作填补了代数几何形式化领域的空白，也为智能体编写软件和后续科学研究提供可复用的验证基础。