Axiom Math称用AI完成Stacks Project形式化验证

事件综述根据 1 篇报道整理，11月6日更新

Axiom Math 宣布已对 Stacks Project 完成形式化验证：公司称其 AI 智能体把这部约 7,654 页的数学文献翻译成约 1,600 万行经 Lean 证明助手逐行检查的代码，并在并行工作时保留定理与定义之间的相互依赖关系。 Axiom 表示为此训练了自有数学模型，并认为这填补了代数几何在形式化数学中的空白，未来研究者可将这些已校验结果作为新证明的基础。上述完成情况与效果均为公司自述，报道未提及第三方复核。

综述由模型根据报道生成，细节以各篇原文为准。