AxiomMath 希望用形式化验证阻止 AI 劣质内容进入数学领域

Axiom Math wants to keep AI slop out of mathematics

AxiomMath 周三宣布已对 Stacks Project 完成形式化验证，希望为 AI 智能体提供可靠的数学基础。其智能体将约 7,654 页数学内容转为约 16 million 行由计算机检查的 Lean 代码，并保留定理与定义之间的依赖关系。公司称，这些已验证结果可供后续数学证明复用，并希望将这一方法扩展到软件开发和科学研究。