Axiom Math 希望用形式化验证阻挡数学领域的 AI 低质内容

Axiom Math 周三宣布已完成 Stacks Project 的形式化验证，希望为 AI 智能体编写软件及未来开展科学研究建立可靠基础。公司让智能体并行工作、自行寻找任务，将约 7,654 页数学内容转为约 16 million 行经计算机检查的 Lean 代码，并保留定理与定义间的依赖关系。Axiom 表示，这些经过验证的结果可供后续证明复用，也希望将这种方法迁移到软件开发。