M2F: Automated Formalization of Mathematical Literature at Scale

M2F (Math-to-Formal) is a framework for translating textbook- and paper-level mathematics into Lean projects that pass machine verification at scale.

Figure 1. High-level overview of M2F and its staged formalization process.

Overview

M2F addresses a central bottleneck in machine-assisted mathematics: the transition from isolated theorem proving to document-level formalization. The framework decomposes this process into two stages. In Stage 1, informal mathematical statements are translated into Lean declaration skeletons, while structural inconsistencies are detected and repaired. In Stage 2, the statement signatures are fixed, allowing the system to focus on proof completion through iterative, verifier-guided repair. This staged design enhances robustness and interpretability while substantially improving end-to-end compilation and verification rates.

Try Quokka (https://quokka.reaslab.io/), our publicly available automated formalization system. Quokka can automatically transform long-form mathematical literature into compilable Lean 4 projects containing formally verified statements and proofs.

At a Glance

Method

Stage 1: Statement Compilation

• Converts informal mathematical statements into Lean declaration skeletons.
• Repairs namespace, type, and signature consistency to ensure project-level validity.
• Allows temporary proof holes to maximize structural coverage before proof repair.

Stage 2: Proof Repair

• Freezes statement signatures to prevent target drift.
• Iteratively closes proof holes with verifier feedback.
• Optimizes proof success under fixed declarations for reliable end-to-end checking.

End-to-End System Figure

Figure 2. End-to-end architecture for document-level formalization with M2F.

Experimental Scope

• Cross-prover benchmark: FATE-H for direct and reproducible comparison of pass rates.
• Long-document setting: large mathematical sources translated into executable Lean projects.
• Core metrics: Pass Success Rate (PSR), verifier-call efficiency, and verifier-normalized cost.

Involvement of Human Experts:

• Checking whether the natural-language theorems extracted from the LaTeX source align with the original text.
• Verifying that the formalized statements correctly match their natural-language counterparts.

Formalized Sources: ReasBook

Books

• R. Tyrrell Rockafellar, Convex Analysis, Princeton University Press, Princeton, 1970, ISBN 0-691-08069-0.
• Jiri Lebl, Introduction to Real Analysis, Volume I, version 6.2, May 23, 2025.
• ...

Paper

• Yurii Nesterov, "Smooth minimization of non-smooth functions," Mathematical Programming, Series A 103, 127-152, 2005, DOI: 10.1007/s10107-004-0552-5.
• ...

Example Demonstration

An end-to-end sample is provided in example/ based on Section 1 (Affine Sets) of Rockafellar's convex analysis. The workflow in this example is: PDF source -> structured JSON -> Lean formalization.

• Structured source input (extracted from PDF): example/section01.json
• Generated Lean files:
  example/Rockafellar_convex_analysis_section01/section01_part1.lean, example/Rockafellar_convex_analysis_section01/section01_part2.lean, example/Rockafellar_convex_analysis_section01/section01_part3.lean, example/Rockafellar_convex_analysis_section01/section01_part4.lean
• Merged entry file: example/Rockafellar_convex_analysis_section01/section01.lean
• Examples of projects generated by M2F: optsuite/ReasBook

This example explicitly starts from PDF parsing output (section01.json) and then performs formalization from JSON to machine-checkable Lean code.

Result Highlights

Long-Document (Book) Extraction Summary

Table 1. Book-level extraction and formalization summary (long-document setting).

FATE-H Across Provers (PSR)

Figure 4. Pass Success Rate (PSR) comparison across provers on FATE-H. PDF version

Table 2. M2F summary results on FATE-H and matched-statement settings.

FATE-H Length and Outcomes

Figure 5. Per-problem proof length and verification outcomes on FATE-H. PDF version

Alignment Analysis

Figure 6. Alignment behavior analysis under the convex setting.

Key Takeaways

• A staged compilation-repair pipeline scales formalization beyond isolated theorem tasks.
• M2F achieves strong fully automatic performance and further improves with lightweight supervision.
• Document-level formalization can reach high verifier pass rates under controlled, reproducible workflows.

Contact

We hope that the package is useful for your application. If you have any bug reports or comments, please feel free to email one of the authors:

• Zichen Wang, zichenwang25 at stu.pku.edu.cn
• Wanli Ma, wlma at pku.edu.cn
• Kun Yuan, kunyuan at pku.edu.cn
• Zaiwen Wen, wenzw at pku.edu.cn

Reference

Zichen Wang, Wanli Ma, Zhenyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen, M2F: Automated Formalization of Mathematical Literature at Scale, arXiv:2602.17016, 2026.

Citation

@article{wang2026m2f,
  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}
}

License

This repository is released under the CC BY-NC 4.0 license
(Creative Commons Attribution-NonCommercial 4.0 International).
See the full terms in LICENSE.