AI创企Axiom完成数学巨著形式化验证
报价宝综合消息AI创企Axiom完成数学巨著形式化验证
AI 数学创企 Axiom Math 周三宣布，已完成对数学界规模最大的文献工程之一"Stacks Project"的完整形式化验证：这部约 7654 页的开源数学参考书，被翻译成约 1600 万行可由计算机逐行检验的代码。
Stacks Project 由哥伦比亚大学数学家约翰·德容于 2005 年发起，此后由全球数学家接力编写，内容从大学水平的代数一路延伸到代数、几何与数论的最前沿课题。它在数学圈地位特殊——同在哥大的数学家彼得·沃伊特曾评价"几乎没有别的工程可与之相比"，并将其比作 20 世纪从地基重建数学的布尔巴基丛书。
所谓形式化验证，是把数学证明改写成名为 Lean 的编程语言代码，再由"证明助手"程序逐行检查逻辑。只要通过检查，证明在逻辑上就无可挑剔。工程师早已用同样的思路验证芯片设计，法国的研究人员也用它找出过家庭补贴计算软件中的漏洞。
对 Stacks 这样的文献来说，难点远不止逐条核对定理：书中的定理与定义层层嵌套、相互引用，验证必须保证整棵依赖树的每一环都站得住脚。Axiom Math 用一支 AI 智能体编队完成了这项浩大工程。
这家估值已达 16 亿美元的公司想解决的是当下 AI 数学产出泛滥的问题：仅上个月，OpenAI 一家就发布了 719 份声称解决数学领域最难问题的手稿，质量良莠不齐，连计算机辅助检查本身也可能出错。Axiom Math 的赌注是，数学不必靠放慢 AI 的速度来自保，而是站上更坚实的地基——让 AI 智能体在经过验证的基础上写软件，最终去做科学。
编译自 TechCrunch，原标题："Axiom Math wants to keep AI slop out of mathematics"
