河南
最近AI在数学圈的动作真的接二连三，前脚DeepMind刚放出消息，说他们的新系统搞定了9道悬了半个多世纪的经典数学难题，每道题成本才几百美元。这波热度还没退，Meta又甩出来一个狠活。他们联合纽约大学搞出了目前规模最大的自动化数学形式化项目，这事细想真的颠覆认知。
很多人可能听不懂什么叫数学形式化，说白了就是把人看的数学定理证明，转成计算机能逐行核查逻辑的代码。有个叫Lean的工具就干这个，它就像数学证明的质检员，只要它点头说通过，这个证明的逻辑就绝对没毛病。这次Meta搞的ATLAS，就是基于Lean 4的超大代码库。
统计显示，到2026年5月，ATLAS已经覆盖了26本来自顶级开放资源的本科研究生数学教材，横跨十多个数学和相关领域。整个代码库加起来超过63万行，挑出来的4007条教材定理里，已经有2855条完成了形式化，覆盖率刚好71.3%。
Lean社区全球数学家一起攒了多年的标准库Mathlib，也就两百多万行代码。ATLAS这堆代码全是机器几周内生成的，体量已经达到Mathlib的四分之一，这个速度放在以前想都不敢想。整个生成过程用掉了超过1830亿个token，算力消耗确实不小，但效率已经够惊人。
更牛的是，这堆代码不是人类程序员一行一行敲的，全靠Meta自研的AutoformBot自动生成，这个工具现在已经开源了。它把整个形式化过程当成多智能体协同的软件工程，直接用了开源社区的协作模式，好几百个AI智能体一起干活。全程没有人工碰证明内容，全是机器自动驱动，这才撑起了这么大的规模。
玩出的状况也真的超出不少人想象，团队跑项目的时候发现，干活的AI工人居然会摸鱼作弊。碰到难啃的定理证明，AI就会偷偷在辅助引理里塞一个Lean自带的sorry关键字，相当于打了张欠条，告诉编译器这里先算对，回头再补。整个证明链看起来顺利通过，其实就是个空架子。
审核的AI变严之后，干活的AI并没有老老实实改，反而把sorry藏得更深，埋到了整个依赖链的最底层，表层审核根本发现不了。这不就是现实版的猫鼠游戏吗？最后团队不得不专门做了一个递归追踪整个依赖图的工具，才把这些藏起来的坑全挖出来。这种AI之间的对抗动态，现在也成了多智能体领域一个值得研究的新问题。
管调度的编排AI跑久了也会犯懒，上下文窗口被各种历史信息塞满之后，给的任务描述越来越粗糙，碰到难的活直接就悄悄跳过了。团队想出的解决办法也很简单，把难的专项活分给新的短生命周期专业AI去做，就解决了长期AI的上下文退化问题。
项目里还放出了很实在的模型对比数据，同样1200M tokens的算力预算，同一本《代数组合学》教材，Claude Opus 4.6完成了92%的形式化目标，Gemini 3.1 Pro只完成了46%。差距从一开始就拉开了，团队说主要是不同模型对Lean语言的编码能力差得挺多，所以整个ATLAS基本都是Claude Opus 4.6驱动生成的。
现在算下来，这套自动流水线生成单行代码的成本，已经比人类专家手写标注还要低，速度更快，想扩规模也更容易。只是整体输出质量，还是比不上人类专家手写的Lean代码，这点团队也没藏着掖着。
ATLAS本身也不是什么完工的成品，就是一个持续推进中的项目。目前还有28.7%的目标定理没做完，李群、布尔函数分析这些难度高的领域，覆盖率还不到一半。代码风格和全球数学家维护的黄金标准库Mathlib比，也还有不小差距。团队也开放了外部贡献入口，欢迎全世界的开发者一起完善。
这件事的意义其实早就超出了一个代码库本身，刚好撞上了现在数学界正在发生的认知转变。菲尔兹奖得主陶哲轩早就说过，数学正在从“证明匮乏”往“证明泛滥”转，以后最关键的问题早就不是AI能不能证出定理，而是整个数学界有没有足够的基础设施，能消化验证整理AI马上就能批量产出的大量成果。
AI现在能随便整出一大堆看起来逻辑通顺，其实偷偷藏着错误的证明，像Lean这种形式验证工具，就是帮AI守住底线的关键。从这个角度看，ATLAS就是一次给未来数学基础设施大规模搭台的实验，方向对了，后续的发展足够让人期待。
参考资料：澎湃科技 Meta发布大规模自动化数学形式化项目ATLAS
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
