arXiv2Formal 首次把 research-paper theorem 的自动形式化拆成可操作子任务

Patel、Saha 与 Flanigan 针对 research-level mathematics 的 autoformalization 提出分解路线：先做不依赖现有库链接的 unlinked formalization，再完成 entity linking，最后调整 types 以通过 type checker。论文同时发布 arXiv2Formal，包含从 arXiv 数学论文抽取并人工形式化的 50 个 Lean theorem，明确把研究论文数学而非教材/竞赛题作为目标。