M2F：大规模数学文献自动形式化
人工智能
2026-02-20 v1
摘要
自动化形式化数学可实现机械验证，但仅限于孤立定理和短代码片段。要实现对教科书和研究论文的规模化形式化，仍面临跨文件依赖、导入解析以及确保整个项目端到端编译等挑战。我们提出 M2F（Math-to-Formal），第一个实现端到端、项目规模自动形式化框架，基于 Lean。该框架包含两个阶段。陈述编译阶段将文档划分为原子块，依据推断依赖进行排序，并修复声明框架直至项目编译，允许证明中存在占位符。证明修复阶段在固定签名下通过目标导向的局部编辑关闭这些空洞。整个过程中，M2F 持续与验证器协作，仅在工具链反馈确认改进后才提交编辑。在约三周时间内，M2F 将长篇数学来源转换为 153853 行、来自 479 页教科书（实分析与凸分析）的 Lean 库，全部形式化为 Lean 声明并附带证明。这代表了教科书规模的形式化进展，通常需要数月乃至数年的专家工作。我们在 FATE-H 上实现了 96% 的证明成功率（相较于强基线的 80%）。这些结果表明，实际的大规模数学文献自动形式化已然可达。完整生成的 Lean 代码可在 https://github.com/optsuite/ReasBook.git 获取。
引用
@article{arxiv.2602.17016,
title = {M2F: Automated Formalization of Mathematical Literature at Scale},
author = {Zichen Wang and Wanli Ma and Zhenyu Ming and Gong Zhang and Kun Yuan and Zaiwen Wen},
journal= {arXiv preprint arXiv:2602.17016},
year = {2026}
}