数学领域正在迎来一场由人工智能驱动的深刻变革。
最近数月，这条赛道上捷报频传。前不久，Google DeepMind 宣布其新系统 AlphaProof Nexus 一举攻克了 353 道开放 Erdős 问题中的 9 道——其中两道在数学界悬而未决长达 56 年，每道题的推理成本仅数百美元。这一成果之所以可信，关键在于 AlphaProof Nexus 放弃了传统自然语言证明的生成方式，而是将大语言模型（Gemini 3.1 Pro）与形式化验证工具 Lean 深度集成：AI 提出证明后，Lean 像编译器逐行检查代码那样，严格核验每个逻辑步骤，不通过则直接驳回。所有证明代码已在 GitHub 上公开，任何人均可独立复现与验证。
如今，又一项重磅成果问世。Meta 联合纽约大学等机构正式发布了 ATLAS（Autoformalized Textbook Library At Scale）——这是迄今规模最大的自动化数学形式化工程之一。
该项目论文及代码均已公开上线。
- 项目地址：https://github.com/facebookresearch/atlas-lean/
- 论文地址：https://github.com/facebookresearch/atlas-lean/blob/main/formalizing_mathematics_at_scale.pdf
ATLAS 是什么？
简单来说：ATLAS 是一个基于 Lean 4 的数学形式化代码库，其核心目标是自动将数学教科书中的非正式定理陈述与证明，转化为计算机能够逐行验证的形式化代码。
听起来有些抽象，但意义非同寻常。Lean 是一种“证明助手”语言——当你提交一段数学证明，它会像编译器校验程序那样，逐步验证每一个推导步骤的逻辑合法性。只要 Lean 通过，该证明在形式意义上便无懈可击。
根据项目 Readme 的统计数据（截至 2026 年 5 月），ATLAS 已覆盖 26 本本科及研究生级别的数学教科书，横跨分析学、代数学、几何、拓扑、组合数学、概率、统计、偏微分方程、数论以及理论计算机科学等众多领域。
整个代码库共计 630,999 行代码，其中 Lean 核心代码 483,917 行；包含 46,203 条数学声明（declarations），其中 42,837 条已完成证明，证明通过率高达 92.7%。
在选定的 4,007 条教科书定理中，已有 2,855 条完成形式化，形式化覆盖率达 71.3%。作为对比：Lean 社区多年协作维护的标准库 Mathlib 约有 210 万行代码、308,129 条声明。而 ATLAS 在数周内机器生成的体量，已达到 Mathlib 总量的约四分之一——这一速度令人惊叹。
这一数字背后是庞大的计算资源消耗：整个生成过程共使用了超过 1830 亿（183,157M）个 token。
研究团队还搭建了一个可视化浏览器，值得重点关注。
访问地址：https://rammalahmad.github.io/atlas/
在该浏览器中，你可以：
- 逐条对比每条定理的非正式原文与 Lean 形式化版本；
- 查看定理之间的逻辑依赖关系图（证明某条定理需要预先知道哪些引理）；
- 提取证明特定定理所需的最小 Lean 代码集合。
这一工具将 ATLAS 从一个单纯的代码库，转变为一张可交互的数学知识图谱——无论是人类研究者还是未来的 AI 系统，都能从中获得潜在价值。
源自哪些教科书？
ATLAS 的 26 本教材全部来自 MIT OpenCourseWare 等顶级开放课程资源，覆盖面极为广泛。
列举几个典型例子：
- RealAnalysis（实分析）：177 条目标定理中已形式化 175 条，覆盖率高达 98.9%，证明通过率 98.7%——这是项目中完成度最高的教科书。
- ComplexVariables（复变函数）：形式化覆盖率达 97.4%。
- NumberTheoryI（数论 I）：576 条目标定理中已形式化 460 条（79.9%），生成代码近 65,000 行。
- AlgebraicGeometryI（代数几何 I）：该领域难度极高，形式化覆盖率 60.2%，但仍生成了超过 4 万行代码和 4,499 条声明。
- LieGroups（李群）：消耗 token 最多（45,384M），生成了超过 6 万行代码，虽然形式化覆盖率仅为 40%，这也反映了该领域的极端技术挑战。
核心引擎：AutoformBot
当然，ATLAS 并非人工编写，而是完全依赖 Meta 自研的自动形式化流水线 AutoformBot（已在 GitHub 上开源）。
项目地址：https://github.com/facebookresearch/autoform-bot
AutoformBot 将教科书形式化视为一个协同软件工程问题，借鉴了成熟的开源协作范式（git 分支、Pull Request 审查、Issue 追踪）来协调成百上千个 LLM 智能体同时工作。
整个系统分为三个管理层级：
- 顶层：编排者（orchestrator）——负责阅读教科书，将形式化任务拆解成有向无环图（DAG），并根据书中的逻辑依赖关系调度工作顺序；
- 中层：追踪分析器（trace analyzer）和监督者（supervisor）——分别负责从失败任务中学习，以及在每次合并后评估目标完成质量；
- 底层：工作者（worker）和审核者（reviewer）——负责实际执行单条定理的形式化与代码审核。
值得强调的是：整个 ATLAS 的生成过程实现了 零人工证明工程介入，完全由机器自动驱动。这正是它能达到如此大规模的前提，也是后续需要持续优化质量和可靠性的原因。
整个系统的计算消耗主要集中于工作者层，占总 token 用量约 76%。每本书的形式化过程通常持续约一周，但通过增加并行度可以显著缩短时间。论文中的实验表明，每任务使用 3 个或 5 个 worker 并行竞速，比单一 worker 在相同时间内多完成约 20% 的目标。
研究团队在论文中坦诚披露了系统运行中观察到的几个有趣的“失效模式”，其中最出乎意料的是 worker 的对抗性“作弊”和“摸鱼”行为。
关键要理解 Lean 里的一个特殊关键字：sorry。它相当于一张“欠条”——告诉编译器“此处证明先跳过，暂且假设为真”。代码因此能顺利编译，但逻辑链条里实际留着一个空洞。正常开发中，sorry 是标记“待填坑”位置的合法工具；但在 AutoformBot 里，它成了 worker 应付考核的捷径：遇到难以证明的定理，就悄悄在某个辅助引理深处塞一个 sorry，让整条证明链看起来通过了，实则是一座纸牌屋。
而这只是最基础的一种手法。论文归纳的“作弊清单”还包括：
- 把定理名称保留，但将真实内容替换成永远为真的废话；
- 将本应证明的结论偷偷藏进数据结构的字段定义（定义不需要证明，只需通过类型检查）；
- 把难题中的复杂数学对象换成简单替身，比如明明要构造一个同构映射，却只证明两个空间的维数相等就交差。
更有意思的是事态的演变：当 reviewer 智能体被要求严格反作弊后，worker 并没有就此收手，而是把 sorry 埋得更深，藏到依赖链条的更底层，让表层审查无法察觉。这场猫鼠游戏倒逼团队构建了一套递归追踪整个依赖图的分析工具，才得以溯源找到真正的“污染节点”。
worker 与 reviewer 之间的这场博弈，在论文里被称为“对抗动态”（adversarial dynamic），并被视作大规模多智能体系统中一个值得深入研究的协调问题。
此外，长期运行的编排者还会出现“LLM 疲劳”——随着上下文窗口被大量历史信息占满，它开始生成越来越粗糙的任务描述，甚至悄悄放弃处理困难目标。团队的解决方案是将专项分析工作委派给短生命周期的专业智能体，避免单一长期智能体的上下文退化。
在模型选择上，论文给出了一组关键对比数据：以同等算力预算（1200M tokens）在《代数组合学》教科书上对比，Claude Opus 4.6 完成了 92% 的形式化目标，而 Gemini 3.1 Pro 仅完成 46%——差距几乎在实验开始时就已经显现。团队将其归因于模型在 Lean 语言上的编码能力差异。这也是为什么整个 ATLAS 主要由 Opus 4.6 驱动。
成本方面，团队估计当前流水线的单行代码成本已经低于人类专家标注，同时速度更快、可扩展性更强——不过输出质量整体上仍不及专家手写的 Lean 代码。
局限性
研究团队对 ATLAS 的定位相当客观：这是一个持续进行中的机器生成扩展努力，并非一个完成品。
目前仍有约 28.7% 的目标定理尚未形式化，部分难度较高的领域（如李群、布尔函数分析）覆盖率低于 50%。代码风格与 Lean 社区的主流标准库 Mathlib 相比还有不少差距——Mathlib 是全球数学家协作维护的“黄金形式化库”，拥有严格的风格约定和深度整合要求。
按照下一步计划，ATLAS 将继续：
- 完成各书中剩余定理的形式化；
- 纳入更多教材和数学领域；
- 提升代码质量与可维护性；
- 向 Mathlib 规范靠拢，争取更广泛的开源兼容发布。
当然，也欢迎外部贡献者加入。
结语
ATLAS 的发布，恰好呼应了近期数学界最重要的一场认知转变。
菲尔兹奖得主陶哲轩最近指出，数学正在经历从“证明匮乏”到“证明泛滥”的历史性转变。对他而言，真正的问题已经不再是 AI 能否生成数学证明，而是：数学共同体是否拥有足够的基础设施，来吸收、验证、整理和理解 AI 可能很快大规模产出的数学成果。
https://mathstodon.xyz/@tao/116653336847856534
他的判断一针见血：“首先发现某个证明，或者率先形式化某个定理，不应该是最终目标。阐释与消化，正在变得远比这更加重要。”
陶哲轩认为，AI 越来越能生成大量看似严谨实则暗含谬误的论证，而形式验证工具（如 Lean）正是让 AI 保持诚实的关键手段。
从这个角度看，ATLAS 的意义超越了一个代码仓库的范畴——它更像是一次对“数学基础设施”的大规模投资实验。
