Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to the complex hierarchy of types and definitions in formal libraries such as Mathlib, while ensuring that generated statements preserve the meaning of the source propositions. Existing approaches struggle because they rely heavily on the model's parametric memory for library-specific knowledge, while common data construction pipelines often resort to filtering single-pass outputs and lack mechanisms for feedback-driven revision. To address these challenges, we introduce MathForm, an autoformalization framework for constructing verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement. Before generation, a retrieval planner gathers relevant definitions and existing formalizations from Mathlib to guide the formalization generator. Generated statements are then revised using compiler diagnostics and semantic-consistency feedback. Using this framework, we construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples across diverse mathematical domains and sources. We then train MathForm-8B through supervised fine-tuning followed by reinforcement learning. Across six benchmarks, MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check (SC) and 72.37% under Consistency Check (CC), outperforming multiple specialized 32B autoformalizers. On the challenging FATE-H and FATE-X subsets, it attains CC pass rates of 63% and 37%, exceeding the strongest specialized baselines in both cases.
Figures & tables
Figure 1: Macro-average Pass@8 (%) across six benchmarks among specialized autoformalizers. MathForm -8B achieves the strongest overall performance within this category despite its smaller model size.
Figure 2: Overview of the MathForm data construction and training pipeline. The system combines Mathlib knowledge retrieval, compilation and semantic verification, and iterative refinement to generate reliable formal data, followed by trajectory reconstruction and training of MathForm -8B.
Figure 3: Distribution of natural-language problem sources in FormalVerse .
Figure 4: Numbers of natural-language-to-formal-language pairs accepted in successive refinement rounds. Later rounds contribute an additional 31.0% of all retained pairs.
AVG
FormalMATH
ProverBench
CombiBench
FATE-M
FATE-H
FATE-X
Model
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
Specialized Autoformalizers
Herald Translator-7B
64.12
27.63
95.29
47.76
78.74
37.36
77.00
5.00
70.67
54.67
42.00
15.00
21.00
6.00
Kimina-Autoformalizer-7B
73.20
34.37
99.29
76.24
96.55
56.32
95.00
16.00
77.33
44.67
43.00
8.00
28.00
5.00
Mathesis-HPO-7B
76.20
34.96
99.06
79.29
97.13
59.77
96.00
15.00
84.00
48.67
50.00
4.00
31.00
3.00
StepFun-Formalizer-7B
58.12
39.55
97.41
81.41
89.66
59.20
79.00
28.00
60.67
52.67
17.00
12.00
5.00
4.00
Table 1: Pass@8 pass rates (%) under Syntax Check (SC) and Consistency Check (CC) for specialized autoformalizers on six benchmarks. AVG is the equally weighted macro-average across all six benchmarks. For each column, the best result is shown in bold and the second best is underlined .
Figure 5: Training dynamics during reinforcement learning. The left panel shows the training reward and its exponential moving average (EMA), while the right panel reports the Mean@3 pass rate on FATE-H over the course of training.
AVG
FATE-M
FATE-H
FATE-X
Method
SC
CC
SC
CC
SC
CC
SC
CC
gpt-oss-120b
Single
27.33
26.43
52.00
51.30
21.00
19.00
9.00
9.00
BoN
42.67
41.10
70.00
69.30
40.00
37.00
18.00
17.00
Feedback
42.57
40.77
68.70
67.30
41.00
38.00
18.00
17.00
Retrieval
32.23
29.00
56.70
52.00
27.00
26.00
13.00
9.00
Table 2: Ablation results for SC and CC pass rates (%) of the refinement pipeline with two generators on the FATE series. Single denotes single-pass generation; BoN denotes Best-of- N ; Feedback denotes feedback-only iteration; and Retrieval denotes retrieval-only single-pass generation. AVG is the equally weighted average over FATE-M, FATE-H, and FATE-X.
AVG
FormalMATH
ProverBench
CombiBench
FATE-M
FATE-H
FATE-X
Training Dataset
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
NuminaMath-LEAN
66.24
41.49
99.53
85.18
96.55
72.41
87.00
25.00
69.33
49.33
35.00
16.00
10.00
1.00
FineLeanCorpus
78.25
46.53
100.00
84.47
98.85
74.71
96.00
29.00
90.67
68.00
53.00
17.00
31.00
6.00
FormalVerse
77.17
60.32
98.82
90.59
98.85
89.66
78.00
36.00
95.33
84.67
62.00
46.00
30.00
15.00
Table 3: Pass@8 SC and CC pass rates (%) of models trained on different datasets across six benchmarks. All models are initialized from Qwen3-8B and trained on 100K examples under the same trajectory reconstruction and training configuration. AVG is the equally weighted macro-average across all six benchmarks. The best result in each column is shown in bold and the second best is underlined .
Judge Model
Accuracy
Precision
Recall
F1
gpt-oss-120b
0.8917
0.8755
0.9133
0.8940
QwQ-32B
0.8567
0.8367
0.8867
0.8609
gpt-oss-20b
0.8500
0.8142
0.9067
0.8579
Table 4: Judge-model reliability on the human-annotated semantic-consistency test set (Mean@3).
Appendix figures & tables4 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 6: Category distribution of the natural-language mathematical problems in FormalVerse .
Table 11
AVG
FormalMATH
ProverBench
CombiBench
FATE-M
FATE-H
FATE-X
Model
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
General-Purpose LLMs
DeepSeek-V4-Pro
78.34
76.54
97.88
96.24
94.83
93.68
85.00
81.00
87.33
87.33
70.00
68.00
35.00
33.00
Qwen3.7-Plus
86.33
83.38
99.29
98.59
100.00
97.70
92.00
87.00
94.67
92.00
78.00
77.00
54.00
48.00
Qwen3-235B-A22B-Thinking-2507
58.94
55.37
91.29
88.24
81.03
75.29
59.00
50.00
71.33
70.67
32.00
30.00
19.00
18.00
Qwen3-32B
43.07
36.55
80.94
72.94
61.49
50.00
43.00
27.00
46.00
43.33
20.00
19.00
7.00
7.00
Appendix
Table 7: Pass@8 SC and CC pass rates (%) of general-purpose LLMs and MathForm -8B across six benchmarks. AVG is the equally weighted macro-average across all six benchmarks. The best result in each column is shown in bold and the second best is underlined .
FATE-M
FATE-H
Model
SC
CC
SC
CC
StepFun-Formalizer-32B
42.67
36.00
16.00
12.00
Goedel-Formalizer-V2-32B
75.33
68.00
38.00
27.00
ReForm-32B
78.67
74.00
50.00
41.00
MathForm -8B
86.67
76.67
54.00
42.00
Appendix
Table 8: Human-evaluation results (%) on FATE-M and FATE-H, based on one randomly sampled candidate per problem. The best result in each column is shown in bold .
While Large Language Models (LLMs) have demonstrated exceptional capabilities in mathematical reasoning, they frequently produce subtle errors that evade human detection. Formal mathematical languages like Lean 4 offer mechanical proof checking, strongly motivating the need for autoformalization: the automatic translation of natural language mathematics into verifiable code. Recent trends indicate that general-purpose LLMs, heavily optimized for standard programming, now outperform smaller models explicitly fine-tuned for Lean. Leveraging this shift, we introduce an agentic autoformalization framework powered by general coding LLMs. At the core of our system is an orchestrator that manages a multi-agent pipeline tailored for research-level mathematics. Because cutting-edge research frequently relies on concepts outside the scope of existing libraries like Mathlib, our system dynamically extends necessary type definitions and validates them via a novel Auxiliary Lemma technique before formalizing the primary theorems. We applied our approach to PutnamBench, producing machine-checked Lean proofs for a random sample of 32 problems. Furthermore, we evaluate our system on five papers from the ACM Symposium on Theory of Computing (STOC) spanning combinatorics, communication complexity, mechanism design, and learning theory, successfully formalizing their main theorems and validating the generated formalizations with human experts; for all five we also formalize the proofs alongside the statements, and notably two of them are proved with no axioms beyond Lean's kernel. All of our formalizations are available at https://beyondthelibrary.github.io/formal_arxiv .
Arshia Soltani Moakhar, Iman Gholami, Max Springer +2
Autoformalization - automatically translating natural language mathematical texts into formal proof language such as Lean4 - can help accelerate AI-assisted mathematical research, be it via proof verification or proof search. I fine-tune Qwen3.5-2B with LoRA for natural language to Lean4 formalization on FineLeanCorpus and consider three training regimes: supervised fine-tuning (SFT) with curriculum learning (difficulty 1 to 10), SFT without curriculum ordering, and reinforcement learning using group relative policy optimization (GRPO) with a cycle consistency reward. Cycle consistency measures how well the meaning of a statement is preserved through a NL to Lean4 to NL' loop, computed as cosine similarity of off-the-shelf sentence embeddings. On an unseen subset of FineLeanCorpus (FLC) and on PutnamBench, RL substantially outperforms both SFT variants (mean cycle consistency 0.669 vs. 0.513 on FLC; 0.561 vs. 0.422 on PutnamBench), while increasing cross-entropy loss by only 0.011 nats, with minimal impact on formalization quality. Curriculum ordering provides no measurable benefit over shuffled training.
Arsen Shebzukhov
Department of Computer Science, Stanford University
We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library At Scale (Atlas) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped with formal verification tools, dependency-aware task scheduling, and collaborative version control, to translate informal textbook prose into machine-checked definitions and proofs. We apply our methods to a corpus of 26 open-access textbooks spanning analysis, algebra, topology, combinatorics, and probability, producing Atlas: a verified library of over 45,000 Lean 4 declarations and 500 thousand lines of code. We release two artifacts: (i) AutoformBot, the open-source multi-agent framework; and (ii) Atlas, the resulting formal library. Our results suggest that autoformalizing the core content of graduate-level mathematics at scale is now economically and technically feasible. This opens the door to the automated verification of both human- and machine-generated mathematics at a research level.
Ahmad Rammal, Niket Patel, Fabian Gloeckle +5
1FAIR at Meta · 2CERMICS, ENPC, Institut Polytechnique de Paris · 3New York University +2