发生了什么
AI at Meta 发布 ATLAS(25+ 本教材，50 万行代码)
为什么值得关注
可重点查看其 formalization harness 的设计与数据规模，判断是否能复用到其他数学/推理任务的自动形式化流程中。
信息来源
以下内容来自公开来源，可打开原文继续核验。
01
ATLAS
Yann LeCun 转发了 Charles Arnal 关于 Meta AI 团队 ATLAS 的发布。ATLAS 是一项自动形式化项目，收录了来自 25+ 本数学教材的 Lean 4 形式化内容，覆盖数十个领域，总计 50 万行代码；同时还开源了一个可扩展的形式化 harness 和配套论文。该工作由 AI at Meta、NYU Data Science 和 Ecole des Ponts 的团队共同推进，作者表示这是一个仍在进行中的项目，并欢迎外部贡献。
打开原始来源 ↗