Axiom Math 完成 Stacks Project 形式化验证，欲为 AI 智能体筑牢数学地基
Axiom Math 宣布已将人类规模最大的数学文献之一 Stacks Project 完成形式化验证，把约 7,654 页内容转写为约 1,600 万行 Lean 代码。该公司称，此举意在为 AI 智能体提供可复用的已验证知识基础，避免数学领域被低质 AI 产出侵蚀。
核心事实
据 TechCrunch 报道，估值 16 亿美元的初创公司 Axiom Math 于周三宣布，已完成对 Stacks Project 的形式化验证。Stacks Project 由哥伦比亚大学数学家 Johan de Jong 于 2005 年发起，是一个开源数学参考库，内容覆盖从本科代数到代数、几何与数论领域的前沿结果。Axiom 称，其 AI 智能体集群将该库约 7,654 页内容转写为约 1,600 万行可被计算机逐行检查的 Lean 代码。
形式化验证的做法是：数学家把证明改写为 Lean 语言代码，再由证明助手逐行核验；若通过，即可认为该证明在逻辑上成立。Axiom 首席执行官 Carina Hong 表示，团队最初并不确定这种“氛围编程”式的方法能否保住 Stacks 的结构之美，最终通过给智能体设定宽松层级、让其并行自主认领任务完成。
背景与影响
报道提到，AI 生成数学成果的速度正在加快，仅 OpenAI 一家上月就发布了 719 篇声称解决难题的稿件，而计算机检查本身也可能出错。Axiom 认为，每个已验证结果都可成为后续证明的积木，减少从零开始的工作。该公司技术团队成员 Ashvin Swaminathan 称，已形式化的数学中存在一大“黑洞”，即代数几何，而这一空白如今得到填补。
Axiom 的目标读者不止数学家。报道称，随着 AI 智能体编写越来越多代码，软件可靠性问题愈发突出，公司押注未来的软件需要建立在已验证的基础之上。Hong 还公开向各家编程公司发出挑战，要求它们在这一规模上开展形式化工作。
限制与来源
上述内容来自 TechCrunch 报道，Axiom 的验证成果、代码规模及技术细节均出自该公司自述，尚未见独立第三方复核。报道未披露该形式化库的开放许可、访问方式与地区可用性，相关安排请以 Axiom Math 官网当前信息为准。本文不构成任何投资建议。