M2F: Automated Formalization of Mathematical Literature at Scale

Autoformalization is often evaluated one theorem at a time. Frontier mathematics exposes a different bottleneck. Before a hard theorem can be proved, a project needs well-modeled definitions, reusable APIs, canonical lemma statements, and stable dependencies. We present M2F (Math-to-Formal), a framework for compiling long mathematical sources into project-scale Lean infrastructure. M2F first turns source-aligned statement skeletons into a Lean project with proof placeholders. It then freezes statement signatures and repairs the remaining holes. Both stages use a verifier-gated accept/revert contract: an edit is committed only when Lean reports improvement under the pinned environment. We evaluate M2F as an artifact-construction system, not as a theorem-snippet prover. The released workspace spans seven source roots across six domains, with 591 generated Lean files and 10{,}637 declarations. It builds end to end, and a strengthened static scan finds no explicit bypass, unsafe, or search-disabling patterns. A two-expert adjudicated audit labels 2{,}023/2{,}089 matched statements as acceptable, and M2F closes all 875 proof obligations in the retained audited proof subset. Reuse, source-order, overlap, and \texttt{mathlib}-compatibility analyses indicate that the generated projects behave as local libraries rather than direct retrieval of existing facts. As a separate fixed-statement Stage~2 probe, M2F solves 96/100 FATE-H instances automatically and two more with human-written natural-language infrastructure hints that expose reusable declarations, not proofs. Together, these results support a statement-first view of large-scale autoformalization.