Axiom Math 完成数学库 Stacks Project 形式化验证

AI 初创公司 Axiom Math 宣布利用并行 AI 智能体集群完成了对著名数学库 Stacks Project 的形式化验证，将其约 7654 页内容转化为约 1600 万行可由计算机验证的 Lean 代码。该项目填补了代数几何在形式化数学领域的空白，让后续数学证明可以直接复用经过校验的定理；团队认为这种形式化验证基底可作为可迁移能力，未来能为 AI 智能体编写无漏洞代码提供可靠的底层依赖。