M2F：数学文献的大规模自动化形式化

数学自动化形式化支持机械化验证，但仍局限于孤立定理和短片段。扩展到教科书和研究论文基本未被解决，因为它需要管理跨文件依赖、解析导入并确保整个项目端到端编译。我们提出 M2F（Math-to-Formal），首个面向 Lean 端到端、项目规模自动形式化的 Agentic 框架。框架分两阶段运行。陈述编译阶段把文档拆为原子块，按推断依赖排序，并修复声明骨架直至项目可编译，允许证明中留占位符。证明修复阶段在固定签名下用目标导向的局部编辑填补这些空缺。两个阶段全程让验证器在环，只有工具链反馈确认改进时才提交编辑。在约三周内，M2F 把 479 页的实分析与凸分析教科书转化为 153,853 行的项目级 Lean 库，完全形式化为带证明的 Lean 声明。这代表教科书规模的形式化，通常需要专家数月或数年。在 FATE-H 上，我们取得 96% 的证明成功率（强基线为 80%）。综合来看，这些结果表明实用的大规模数学文献自动形式化已触手可及。我们运行生成的完整 Lean 代码见 https://github.com/optsuite/ReasBook.git。