数学证明的自动化验证正在迎来里程碑式的突破。Meta联合纽约大学等机构发布了ATLAS项目，这是迄今为止规模最大的自动化数学形式化工程之一。该项目将26本本科及研究生级别的数学教科书自动翻译成Lean 4形式化代码，让计算机能够像检查代码一样逐行验证数学证明的逻辑正确性。这一成果意味着AI在数学领域的应用已从简单的符号计算迈向了更深层次的逻辑推理。ATLAS的核心价值在于其惊人的规模和效率。整个代码库共计630,999行代码，其中Lean核心代码达483,917行，包含46,203条数学声明，其中42,837条已完成证明，证明通过率高达92.7%。在被选定的4,007条教科书定理中，已有2,855条完成形式化，覆盖率达71.3%。作为对比，Lean社区多年协作维护的标准库Mathlib约有210万行代码和308,129条声明，而ATLAS在数周内机器生成的体量已达到Mathlib总量的约四分之一。这一速度背后是巨大的计算投入——整个生成过程消耗了超过1830亿个token。从技术视角看，ATLAS的突破在于将大语言模型与形式化验证工具Lean深度结合。AI负责将教科书中的非正式定理陈述和证明翻译为计算机可验证的代码，Lean则像编译器一样逐步骤核查逻辑合法性。项目覆盖的教材全部来自MIT OpenCourseWare等顶级开放课程资源，横跨分析学、代数学、几何、拓扑、组合数学、概率、统计、偏微分方程、数论以及理论计算机科学等众多领域。这种跨学科的覆盖范围使ATLAS不仅是一个代码库，更成为一张可导航的数学知识图谱。ATLAS团队还构建了可视化浏览器，用户可以在其中对比每条定理的非正式原文与Lean形式化版本，浏览定理之间的逻辑依赖关系图，甚至提取证明特定定理所需的最小Lean代码集合。这一工具对人类研究者和未来的AI系统都具有潜在价值。随着形式化数学库的不断扩展，AI在数学发现中的角色将从辅助验证逐步演进为主动探索，而ATLAS正是这条道路上的一块重要基石。对于AI从业者而言，关注这一方向意味着把握住数学与AI交汇处的下一个风口。