M2F: Automated Formalization of Mathematical Literature at Scale
Authors: Zichen Wang, Wanli Ma, Zhenyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen
Organizations: School of Mathematical Sciences, Peking University · Beijing International Center for Mathematical Research, Peking University · Huawei Technologies · Center for Machine Learning Research, Peking University
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.
Figures & tables
Figure 1: The M2F pipeline for project-scale automated formalization.
Corpus
Sections
Pages
Blocks
Decls
Holes
Real Analysis
36
312
416
1195
339
Convex Analysis
15
140
560
2620
499
Paper
6
27
67
301
37
FATE-H
–
–
–
100
100
Table 1: Corpora and scale. Blocks is the number of Stage 1 atomic blocks. Decls is the number of generated declarations after Stage 1. Holes is the number of candidate matched-statement proof obligations for Stage 2.
End-to-end artifact
Matched-statement Stage 2
Corpus
Blocks
PB
Files
Decls
LoC
Holes
Closed
PSR (%)
Real Analysis
416
✓
49
1195
34327
339
339
100
Convex Analysis (Sec. 1–15)
560
✓
164
2620
105682
499
499
100
Paper
67
✓
28
301
13844
37
37
100
Total (long-form)
1043
✓
241
4116
153853
875
875
100
Table 2: End-to-end artifacts and proof progress under matched statements. PB indicates that the final project builds under E . A concrete workflow walkthrough and code overview are provided in Appendix D .
Metric
Real Analysis
Convex Analysis
Paper
SCC (%)
100
100
100
ARR (rounds)
0.42
0.08
0.20
PB
✓
✓
✓
Table 3: Stage 1 statement compilation. PB indicates whether the final project builds under E (allowing sorry ).
Method
Real Analysis
Convex Analysis
Paper
One-shot
45.45
63.94
46.15
Diagnostics-only
100
95.45
13.85
No replanning ( C=1 )
100
90.91
46.97
M2F (full Stage 2)
100
100
100
Table 4: Stage 2 ablations under matched statements on fixed slices (one dataset file per long-form corpus, selected and then fixed; slice identifiers are reported in Appendix A.4 ). PSR is computed on holes within each slice; full-corpus results are in Table 2 .
Appendix figures & tables11 assets
Supplementary material from the paper’s appendix.
Appendix
Artifact
Contents
Primary use
Per-call model log
Full stdout/stderr for one model invocation, including effective prompt, tool-wrapper outputs, and emitted diffs; may also include token markers
Per-call auditing/debugging; token backfill from stable markers
Progress checkpoint (JSON)
A single resume cursor (e.g., next item or next file) plus minimal run identifiers
Crash-safe resumability without reprocessing completed targets
History store (JSONL)
Compact per-target records across retries (plan summaries, key errors, selected fields)
Debugging and optional continuity context for later attempts
Metrics event log (JSONL)
Append-only event stream with run/item/file boundaries, verifier checks, and oracle/model-call outcomes
Primary source for paper metrics and verifier/oracle call accounting
Metrics summary (JSON)
Run-end aggregates that mirror the final run_end event payload
Quick run-level accounting without scanning JSONL logs
Token backfill (JSONL)
Per-target token totals reconstructed from stable token markers in per-call logs
Robust token accounting when metrics events omit per-call token fields
Appendix
Table 6: Instrumentation artifacts: content and primary use.
Key
Meaning / used for
index
Stable integer identifier; defines iteration order and is used as the primary resume cursor.
label
Human-readable label (e.g., “Lemma 1.1”); used in logs and for locating targets.
env
Coarse type tag (e.g., definition vs. proposition); used for filtering which items are proof targets.
number_components
Numbering decomposition used as a fallback for deterministic target positioning.
extracted_labels
Source-level labels attached to the item; helpful for traceability and context.
context
Structured section metadata (chapter/section titles and indices) used for deterministic file/position inference.
Appendix
Table 7: Dataset record keys (semantic schema).
Field
Meaning
ts
UTC timestamp (ISO8601).
pipeline
Pipeline tag (e.g., proof or final).
run_id
Run identifier linking to the metrics event log.
lean_file
Lean file identifier (relative path or logical name).
Table 8: History record fields (top-level schema).
Corpus
Stage
Targets
Solved
Total verifier calls
Calls/solved
Notes
Textbooks: Real Analysis
1
416
416
592
1.42
SCC =100% sorry allowed
2
339
339
628
1.85
Matched statements PSR =100%
Textbooks: Convex Analysis
1
560
560
605
1.08
SCC =100% sorry allowed
2
499
499
1065
2.13
Matched statements PSR =100%
Paper
1
67
67
81
1.20
SCC =100% sorry allowed
2
37
37
77
2.08
Matched statements PSR =100%
Appendix
Table 9: Total verifier calls and verifier-normalized cost.
Figure 3: FATE-H per-problem code length (non-empty lines) and outcome category. Colors indicate outcome: green = solved automatically, yellow = solved with lemma-map supervision, red = unsolved; the single wrong-statement instance is shown with a distinct style (see § 6.4 ).
Figure 4: System capability manifesto (workflow). A verifier-in-the-loop pipeline that turns PDF-derived structure into a buildable Lean project with (i) provenance anchoring for statement auditability, (ii) human gatekeeping at governance points, and (iii) accept/revert refinement driven solely by Lean diagnostics, yielding a queryable repository of verified declarations rather than isolated one-off proofs.
Figure 5: System capability manifesto (navigability and locality). Rockafellar Convex Analysis (§1–§15) is re-indexed into a ToC-faithful Lean project. The right panel is an indented file tree (not full paths) illustrating structure-preserving splitting (e.g., a single source section expanded into many _partK modules) while keeping a stable section module for downstream imports and verifier-local edits.
Indicator
Real Analysis
Convex Analysis (§1–§15)
Paper
Max structure-preserving split factor
6-way
23-way
10-way
Unique imported modules (approx.)
50
160+
25+
Provenance anchors in docstrings (approx.)
400+
600+
70+
Remaining sorry (closure)
0
0
0
Appendix
Table 13: System capability manifesto (governance at scale). Indicators that emphasize (i) edit locality via structure-preserving splitting, (ii) dependency governance via an inspectable import footprint, and (iii) auditability via provenance anchors attached to declarations. Scale (files/decls/LoC, PB/PSR) is reported in Table 2 .