Axiom Math 形式化验证开源数学库 Stacks Project

Axiom Math 宣布利用多智能体系统完成了对开源数学项目 Stacks Project 的形式化验证，将其约 7,654 页内容转译为约 1,600 万行经计算机检查的 Lean 代码。该成果填补了代数几何领域在形式化数学上的空白，团队通过自研数学模型让智能体在松散层级下并行分配任务并保持引用一致性。Axiom 计划将该验证成果作为底层基石，未来逐步推广至代码无错验证和科学探索领域。