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

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

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

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