主要证据
- M2F: Automated Formalization of Mathematical Literature at ScaleS1 · 主要研究来源 · 论文 · 2026-02-19
- M2F autoformalization frameworkS1 · 主要研究来源 · 代码仓库
- ReasBook generated Lean formalization projectsS1 · 主要研究来源 · 形式化工件
M2F 将自动形式化从孤立定理扩展到机器检查的 Lean 项目
M2F 首先把长篇数学文档翻译为按依赖排序的 Lean 声明骨架，并修复项目层面的结构不一致；随后固定命题签名，利用验证器反馈迭代填补证明缺口。配套 ReasBook 仓库公开了由教材和研究论文生成的形式化项目。
发生了什么？
M2F 论文报告了一套“命题编译 + 证明修复”的两阶段管线，将 479 页实分析与凸分析材料转化为 153,853 行 Lean 项目，并在完全自动设置下于 FATE-H 达到 96% 的证明成功率；生成的 Lean 代码已公开。
为什么重要？
项目级自动形式化把自动化单位从“一次处理一道题”转变为具有共享定义和依赖关系的完整数学文献，这是将大规模非形式数学语料转化为可复用形式库的重要前提。
重要性说明：M2F 将自动形式化从单个定理命题推进到具有依赖关系的文档级与项目级 Lean 生成，把导入、声明、证明缺口与整个项目的编译统一纳入同一工作流。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 自主主导
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 非形式化, 形式化, 混合
- AI 贡献
- 系统自动翻译命题、修复声明并填补证明缺口，同时利用 Lean 工具链反馈决定项目修改是否被接受。
- 人类贡献
- 研究者设计分阶段形式化管线、准备源文档与评测协议，并报告由人类检查抽取的自然语言定理及其形式命题是否与原始数学内容一致。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- m2f, reasbook, lean
- 机构
- peking-university
- 数学问题
- project-scale-autoformalization, mathematical-literature-formalization
- 方法
- autoformalization, dependency-ordering, verifier-guided-repair, proof-repair, lean
全部来源与工件
- M2F: Automated Formalization of Mathematical Literature at ScaleS1 · 主要研究来源 · 论文 · 访问于 2026-09-11
- M2F autoformalization frameworkS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
- ReasBook generated Lean formalization projectsS1 · 主要研究来源 · 形式化工件 · 访问于 2026-09-11
验证历史
- 2026-02-19 · 论文已发布 · E2 · 研究记录
arXiv 论文发布 M2F，并报告项目级形式化与 FATE-H 结果。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
M2F 与 ReasBook 公开仓库提供框架、示例和生成的 Lean 项目。machine-checked 指发布工作流中的 Lean 编译与证明检查，并不表示每一项生成形式化都获得独立语义审查。
更正
当前没有记录的更正。