**Meta利用AI将数学教材翻译为超大规模Lean库，消耗1830亿token**

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

> Meta利用AI技术，将大量数学教材内容翻译成形式化Lean代码库，该过程消耗了高达1830亿token。这一举措旨在为AI驱动的数学研究和定理证明提供结构化数据支持，推动数学与AI的深度融合。文章还提及了近期AI在数学领域的突破，如Google DeepMind的AlphaProof Nexus系统解决了多个长期未解的数学问题。

**来源信息**
- **来源**：机器之心：文章库（API）
- **分类**：ai-products
- **发布时间**：2026-05-29 13:29（北京时间）
- **原文**：[打开原文](https://www.jiqizhixin.com/articles/2026-05-29-4)