M2F first translates long mathematical documents into dependency-ordered Lean declaration skeletons and repairs project-level structural inconsistencies, then freezes statement signatures and iteratively closes proof holes using verifier feedback.
The M2F paper reported a two-stage statement-compilation and proof-repair pipeline that converted 479 pages of real- and convex-analysis material into a 153,853-line Lean project and achieved 96% proof success on FATE-H in its fully automatic setting; generated Lean code was released publicly.
M2F first translates long mathematical documents into dependency-ordered Lean declaration skeletons and repairs project-level structural inconsistencies, then freezes statement signatures and iteratively closes proof holes using verifier feedback. The companion ReasBook repository exposes generated formalizations from textbooks and research papers.
Project-scale autoformalization changes the unit of automation from one problem at a time to coherent mathematical literature with shared definitions and dependencies, a prerequisite for turning large informal corpora into reusable formal libraries.
Significance rationale: M2F moved automated formalization from single theorem statements toward dependency-aware, document- and project-scale Lean generation, addressing imports, declarations, proof holes and whole-project compilation as one workflow.
—
The arXiv paper introduced M2F and reported project-scale formalization and FATE-H results.
The public M2F and ReasBook repositories expose the framework, examples and generated Lean projects. Machine-checked refers to Lean compilation and proof checking in the released workflow; it does not establish independent semantic review of every generated formalization.
No corrections recorded.
