← All papers
First page of M2F: Automated Formalization of Mathematical Literature at Scale

M2F: Automated Formalization of Mathematical Literature at Scale

Zichen Wang, Wanli Ma, Zhenyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen

cs.AI Feb 19, 2026 · v1
M2F is an agentic, verifier-in-the-loop framework that autoformalizes textbook-scale mathematics into compiling Lean projects with proofs.
Automated formalization of mathematics enables mechanical verification but remains limited to isolated theorems and short snippets. Scaling to textbooks and research papers is largely unaddressed, as it requires managing cross-file dependencies, resolving imports, and ensuring that entire projects compile end-to-end. We present M2F (Math-to-Formal), the first agentic framework for end-to-end, project-scale autoformalization in Lean. The framework operates in two stages. The statement compilation stage splits the document into atomic blocks, orders them via inferred dependencies, and repairs declaration skeletons until the project compiles, allowing placeholders in proofs. The proof repair stage closes these holes under fixed signatures using goal-conditioned local edits. Throughout both stages, M2F keeps the verifier in the loop, committing edits only when toolchain feedback confirms improvement. In approximately three weeks, M2F converts long-form mathematical sources into a project-scale Lean library of 153,853 lines from 479 pages textbooks on real analysis and convex analysis, fully formalized as Lean declarations with accompanying proofs. This represents textbook-scale formalization at a pace that would typically require months or years of expert effort. On FATE-H, we achieve $96\%$ proof success (vs.\ $80\%$ for a strong baseline). Together, these results demonstrate that practical, large-scale automated formalization of mathematical literature is within reach. The full generated Lean code from our runs is available at https://github.com/optsuite/ReasBook.git.

Automated formalization of mathematics has been limited to isolated theorems and short snippets. Scaling to textbooks and research papers requires managing cross-file dependencies, resolving imports, and ensuring entire projects compile end-to-end.

M2F (Math-to-Formal) is the first agentic framework for end-to-end, project-scale autoformalization in Lean. It operates in two stages: a statement compilation stage that splits documents into atomic blocks, orders them by inferred dependencies, and repairs declaration skeletons until the project compiles (allowing proof placeholders); and a proof repair stage that closes holes under fixed signatures using goal-conditioned local edits. Throughout both stages, edits are committed only when Lean toolchain feedback confirms improvement.

In approximately three weeks, M2F converts 479 pages of textbook material (real analysis and convex analysis) into a Lean library of 153,853 lines with 4,116 declarations across 241 files. On FATE-H, it achieves 96% proof success versus 80% for a strong baseline.