Axiom Math用AI智能体完成数学百科形式化

时间：2026年11月4日 地点：美国加州帕洛阿尔托，Axiom Math；美国纽约哥伦比亚大学，Stacks Project 诞生地 人物：Axiom Math 团队；哥伦比亚大学数学家Johan de Jong（Stacks Project发起人）；数学家Peter Woit 事件详情：Axiom Math 宣布发布 Stacks Project 的完整 Lean 形式化版本。官方称，这份约7500页的开源数学参考书被转换为约1600万行代码，全部由 Lean 内核逐行校验，是迄今规模最大的、集成可复用的形式化数学库。研究人员和 AI 智能体现在可以把其中的定义与定理直接导入新的形式化证明，每个 Lean 声明都能通过 Stacks 的永久标签回链到原文对应的段落。据 TechCrunch 报道，这家估值16亿美元的初创公司用一支 AI 智能体队伍完成了这项工作，把 Stacks Project 约7654页内容翻译成约1600万行经计算机检查的代码。 背景：Stacks Project 由哥伦比亚大学数学家 Johan de Jong 于2005年发起，定位是现代代数几何的开源参考书，数百位数学家参与撰写，从大学代数一路写到代数、几何和数论的前沿结果，被数学家 Peter Woit 称为再没有别的东西能与之相比，并拿来与重建现代数学基础的 Bourbaki 文集相提并论。形式化验证的逻辑是把证明改写成 Lean 这类程序设计语言里的代码，再由证明助手检查代码是否成立；此前现代代数几何很难走这条路，因为一个当代证明往往要调用交换代数、概形、层、上同调和代数栈上一长串定理。Axiom Math 此前已在2026年10月27日发布有限简单群分类的 Lean 形式化。 影响：对 AI 参与数学而言，这是一次规模上的跃迁。Axiom 官方称，把如此体量的语料形式化只有靠 Lean 和 Mathlib 社区多年积累的数学库与抽象层才可能做到，他们为此部署了分层的多智能体系统，不同智能体分别承担翻译陈述、检索 Mathlib 现有抽象、构造证明、解决前置依赖等职责，在依赖图上并行推进，再通过多智能体审计、与原文的语义比对，以及每条定义必须能对接下游定理的严格要求，保证形式化忠实于原始数学。它已经实质改动过原始文献：官方称这套系统在 Stacks Project 中发现了数十条需要局部修正的陈述，包括缺失的前提条件、正特征下的边界情形，以及在原有全称表述下并不成立的断言，智能体为这些断言构造了显式反例。产业层面，TechCrunch 的观察是，上个月 OpenAI 放出719篇声称解决该领域最难问题的手稿，而用于确认这些结果的机器检查本身也可能出错；Axiom Math 卖的正是这一层保险。 总结：Axiom Math 用一支 AI 智能体队伍，把人类花了约二十年写成的数学百科搬进了证明助手，产出1600万行可机器校验的 Lean 代码。这套底座的价值不在于替数学家出题，而在于让智能体产出的数学结论能被逐条检查。对国内模型团队来说，这条路径把AI会不会做数学的竞赛，推进到了AI产出的数学能不能被验证的新阶段，而后者才是能否进入严肃科研流程的门槛。边界也要看清：形式化只覆盖已经写下的数学，Stacks Project 仍由 de Jong 与社区维护，2026年10月21日 de Jong 曾要求暂时不要把 AI 生成的评论和拉取请求直接提交到上游仓库，Axiom Math 表示自己的形式化、反例与修正都保留在独立仓库中。另外，1600万行代码的忠实性目前主要由 Axiom Math 自己的审计流程保证，外部独立复核仍在进行。 常见问题： 问：Stacks Project 是什么？ 答：由哥伦比亚大学数学家 Johan de Jong 于2005年发起的开源数学参考书，数百位数学家参与撰写，覆盖现代代数几何，被拿来与 Bourbaki 文集相提并论。 问：形式化验证有什么用？ 答：把证明改写成 Lean 这类语言里的代码再由证明助手检查，让智能体产出的数学结论能被逐条校验，而不是只能靠人读。 参考来源： Axiom Math 官方发布（Stacks Project 形式化） https://axiommath.ai/research/the-stacks-project-formalized/ TechCrunch：Axiom Math wants to keep AI slop out of mathematics https://techcrunch.com/2026/11/05/axiom-math-wants-to-keep-ai-slop-out-of-mathematics/ 品玩：Axiom Math完成Stacks Project形式化验证 https://www.pingwest.com/w/319309 C114：Axiom Math完成Stacks Project形式化验证 http://www.c114.net.cn/ainews/142760.html 智读：Axiom Math完成Stacks Project形式化验证 https://www.zhiding.cn/models/2026/1106/3204995.shtml Dataist：AxiomMath verifies the Stacks Project to keep AI slop out of math https://dataist.ai/news/axiommath-verifies-the-stacks-project-to-keep-ai-slop-out-of-math/ 网易：650多人编写20年的数学百科全书 华人初创用AI将其转化为可验证代码 https://m.163.com/dy/article/LB07I5C405119734.html Gate：Axiom Math 使用 1600 万行 AI 程序代码验证 Stacks Project https://www.gatenode.irish/zh-tw/news/detail/axiom-math-verifies-stacks-project-with-16-million-lines-of-ai-code-25435263