AI 精选动态
智能评分 71
ATLAS
AI 推荐理由
可重点查看其 formalization harness 的设计与数据规模，判断是否能复用到其他数学/推理任务的自动形式化流程中。核心解读
Yann LeCun 转发了 Charles Arnal 关于 Meta AI 团队 ATLAS 的发布。ATLAS 是一项自动形式化项目，收录了来自 25+ 本数学教材的 Lean 4 形式化内容，覆盖数十个领域，总计 50 万行代码；同时还开源了一个可扩展的形式化 harness 和配套论文。该工作由 AI at Meta、NYU Data Science 和 Ecole des Ponts 的团队共同推进，作者表示这是一个仍在进行中的项目，并欢迎外部贡献。