Axiom Math 完成 Stacks Project 的形式化验证

估值 16 亿美元的初创公司 Axiom Math 宣布正式形式化验证 Stacks Project，将其约 7,654 页内容翻译成约 1600 万行 Lean 代码并逐行通过证明助手检查。公司让 AI 智能体在松散层级下并行工作、自行认领任务，并自研擅长数学的模型，填补了代数几何领域形式化数学的空白；Axiom 认为这些已验证的数学可成为智能体构建软件的基础。