# Meta 烧了 1830 亿 token，把 26 本数学教材翻译成了机器可验证的 Lean 代码库

> 原标题：消耗1830亿token，Meta用AI把数学教材翻译成了一个超大Lean库

- 来源：机器之心 · 公众号
- 发布时间：2026-05-29T04:04:00.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/30500
- 原文：https://mp.weixin.qq.com/s?__biz=MzA3MzI4MjgzMw==&mid=2651035616&idx=2&sn=bbe00851e5fd7202b859a7217f6c3a08

## 摘要

Meta 放出了一个叫 ATLAS 的数学形式化库，用 Lean 4 语言把 26 本数学教材里的定义和证明搬了进去。整个工程消耗了 1830.57 亿个 token，生成了约 63 万行代码，包含 46203 条声明。其中 42837 个证明已经跑通，证明通过率 92.7%。说白了就是让 AI 把教科书上的数学推理，转成机器能严格检查的代码，以后训练...

## 推荐理由

HKR三项都站得住：token量、Lean库规模和已验证证明数都是硬数字。没给P1是因为这还是个偏专的研究开源发布，不是通用模型或产品级发布。

## 锐评

Meta 放出的 ATLAS 库，简单说就是把教科书里的数学定义和证明，用 Lean 4 这种形式化语言重写了一遍，让机器能逐行检查推理有没有漏洞。整个工程跑了 1830.57 亿个 token，生成了约 63 万行代码，包含 46203 条声明，其中 42837 个证明已经跑通，通过率 92.7%。这个量级说明他们不是小打小闹，是真想铺一个能用的数学知识底座。

不过得打几个折。第一，原文因为环境异常没加载出完整内容，我们看不到他们用了什么模型、怎么拆任务、人工改了多少。第二，92.7% 的通过率看着高，但剩下没跑通的 7.3% 是卡在哪儿、是不是关键定理，正文没交代。第三，1830 亿 token 的消耗量很大，如果用的是顶级大模型，成本不会低，但具体数字缺失。

对做 AI 推理的人来说，这个库的价值在于它是一块现成的训练料——以后训模型做数学证明，可以直接拿这些对齐过的代码当教材。但现阶段别把它当成“数学全自动形式化”的成熟方案，更像是一次大规模工程验证，告诉我们这条路能走，只是还没算清楚账。