Axiom Math以形式化验证防止AI低质内容进入数学

在生成式人工智能频繁宣称取得数学突破但可靠性受质疑的背景下，初创公司Axiom Math于周三宣布，已完成对大型开放数学资源Stacks项目的形式化验证，将约7654页人工撰写内容转化为约1600万行经Lean证明助手逐行检查的代码。Stacks项目由哥伦比亚大学数学家Johan de Jong于2005年发起，覆盖代数、几何与数论，从本科代数延伸到前沿成果，被同行比作20世纪重建数学基础的布尔巴基丛书。Axiom Math由退出斯坦福数学博士项目的25岁创业者Carina Hong于2025年3月创立，并于同月完成由Menlo Ventures领投的2亿美元A轮融资，被视为估值16亿美元的初创公司。公司使用人工智能代理并行完成翻译，并自训数学模型以保留定理和定义之间复杂的依赖关系。该成果填补了代数几何等形式化数学的重要空白，为研究者提供可复用基础。Axiom Math认为，经机器验证的数学库可成为人工智能代理编写软件、开展科学研究时的可靠底座，从而降低其生成错误证明、漏洞代码和安全风险的概率。菲尔兹奖得主陶哲轩指出，形式化证明越多，越能支撑更多证明生成。Axiom Math强调，未来人工智能需要高质量、可复用知识体系，才能持续拓展能力边界，而非陷入低质生成循环。