MathAtlas：野外自动形式化基准

现有自动形式化基准多集中于奥林匹克或本科数学，研究生及以上层级研究匮乏。本文提出 MathAtlas，首个大规模野外研究生级数学自动形式化基准，含约 5.2 万条定理、定义及证明，源自 103 本教材。其独创性地引入含约 17.8 万关系的数学依赖图，支持依赖感知系统评估。实验表明该基准极具挑战性：最强基线在定理陈述上正确率仅 9.8%，且模型性能随依赖深度增加显著下降，在最深依赖子集上正确率低至 2.6%。