APE-Bench I 把 AI formal math 从单定理证明推进到真实 Mathlib 文件级 proof engineering

APE-Bench I 从真实 Mathlib4 commit history 构建 file-level tasks，覆盖 feature addition、proof refactoring 与 bug fixing，而不是只评测静态 isolated theorem。作者同时提出 Eleanstic，用于跨多个 Mathlib 版本并行验证。实验显示 frontier LLM 对 localized edits 已有较强能力，但一旦任务涉及复杂 proof engineering，性能显著下降。