AxiomMath宣布验证Stacks Project——TechCrunch

AxiomMath宣布完成对Stacks Project的形式化验证。Stacks Project是一个大型开放数学成果库。据TechCrunch报道，该公司的AI智能体将项目约7,654页内容转换为约1,600万行Lean代码，并由计算机证明助手完成验证。

检查数学证明

数学形式化是指用Lean编程语言重写证明。一个特殊程序——证明助手——逐行检查代码。如果检查成功，数学家就可以认为该证明在逻辑上是正确的。

Stacks Project由哥伦比亚大学数学家约翰·德容于2005年创建，作为一项开放参考资源。此后，数学家不断为其补充材料，内容涵盖大学代数以及代数、几何和数论中的复杂主题。数学家彼得·沃伊特曾将该项目的重要性与布尔巴基丛书相提并论，后者在20世纪从基础开始构建数学。

这项工作的复杂性不仅在于检查单个定理。Stacks Project中的定义和结果彼此关联，因此团队在处理约1,600万行Lean代码时必须保留所有这些关联。

更多最新消息请关注 UA.News Telegram 频道 Telegram.

新证明的基础

AxiomMath技术团队代表阿什温·斯瓦米纳坦表示，这一成果填补了形式化数学中的一大空白，尤其是在代数几何领域。他说，希望使用Lean验证该领域新研究成果的研究人员如今已有开展这项工作的基础。

该公司认为，经验证的数学成果可以成为新证明可重复使用的构件，也可以成为AI智能体将要使用的基础设施的基础。创始人兼首席执行官卡琳娜·洪表示，智能体需要一个可靠的知识库，才能在不受早期不成功工程决策所埋下的错误影响的情况下发展它。

洪在离开斯坦福大学数学博士项目后，于2025年3月创立了该公司。3月，AxiomMath在由Menlo Ventures领投的A轮融资中筹集了2亿美元。