LLM-based auto-formalization systems can now generate formally verified Lean code at unprecedented rates. However, a formalization advances mathematical research only when further mathematical results can be built on it, especially when its definitions and helper lemmas are general enough to be imported and used idiomatically. We propose definition grounding, where definition formalizations are continuously judged and revised, as a method to ensure formalization quality. We find that agents formalizing definitions from textbook text often produce definitions that later statements cannot use, and only 25%-50% of their definition sets are compatible with all later statements. However, clarifying the informal definitions can improve this rate up to 77.5% averaged over all models. Furthermore, stating a small set of basic properties without proving them can improve model judges' capability to detect definitions with compatibility issues, at only about 11% of the definition formalization cost. These results are verified with ReuseBench, a benchmark we curated for formalizing new mathematical fields and theories.
Figures & tables
Theory
Source
D
S1
S2
S3
S4
S5
Markov chain mixing times
Levin and Peres (2017)
20
24
14
9
14
13
Random walks on graphs
Levin and Peres (2017)
13
15
12
9
8
5
Curie–Weiss model
Friedli and Velenik (2017)
11
12
13
8
7
5
Nets, covering numbers & singular values
Vershynin (2026)
9
16
14
6
7
4
Linear and Reed–Solomon codes
Guruswami et al. (2025)
14
15
13
7
7
6
Symmetric and Schur polynomials
Grinberg (2025)
14
16
11
9
8
9
Table 1: Number of definitions in D and of statements in each layer S1,…,S5 of every theory in ReuseBench.
Witness rate (%)
Full pass
Model
S1
S2
S3
S4
S5
rate (%)
Source
GPT 6 Astra
6.3
18.1
10.8
11.7
15.2
43.8
GPT 5.6 Sol
5.2
18.0
14.1
16.9
19.2
31.2
Claude Fable 5.1
4.8
10.3
5.6
6.2
3.8
50.0
Claude Opus 5
5.5
6.5
6.2
9.0
6.9
50.0
Table 2: Witness rate in S1,…,S5 and full pass rate of the definition formalizations written by each model, given access to the source text (Source) and the cleaned statements (Cleaned), averaged over all 8 theories. Full pass rate means the percentage of definition formalizations with L(D˙)=True , i.e., that are fully compatible.
Baseline
D ( J0 )
+S1 ( J1 )
+S2 ( J2 )
+S3 ( J3 )
+S4 ( J4 )
Accuracy
0.62
0.65
0.85
0.82
0.82
0.81
AUC
0.62
0.79
0.85
0.85
0.84
0.87
Precision
0.62
0.78
0.86
0.82
0.86
0.86
Formalization cost (USD)
–
$4.32
$0.27
$0.30
$0.24
$0.26
Judge cost (5 repeats)
–
$0.17
$0.21
$0.27
$0.32
$0.35
Table 3: Accuracy, AUC and Precision of the baseline (all True ) and of the judges J0,…,J4 against the compatibility label L(D˙) , over all 8 theories.
Figure 1: Precision-recall curves of the judges J0,…,J4 against the compatibility label L(D˙) , over all 8 theories, thresholding the number of accepting calls out of 5.
We introduce a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness. Unlike most verification methods, which rely on LLMs or trained models, our method combines LLM-based semantic review with mechanical numerical and vacuity checks, providing checkable feedback and detecting errors missed by LLM judges. We apply this method, along with our Extract-Verify-Proof autoformalization pipeline, to construct the Formalized Library of Mathematical Functions (FLMF), a partial formalization of the NIST Digital Library of Mathematical Functions (DLMF). On three labeled datasets, our method achieves the lowest accepted-error rate among the evaluated methods, measured as the fraction of incorrect statements accepted by the verification method. Expert review of the results also identifies translation and source defects in existing datasets. Code available at https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git.
Anna Mei, Michael R. Douglas
Harvard University · CMSA, Harvard University and AletheAI, Inc
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
Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions. We introduce PaperFormalizer, a Lean-based agentic pipeline that helps authors find and close such gaps in their own papers and turn each paper into a Lean-verified version. Starting from the LaTeX source, PaperFormalizer transcribes the paper into a dependency graph of statements, audits each statement in natural language for faithfulness, ambiguity and correctness, and then formalizes and proves the statements in Lean against Mathlib, optional domain libraries and the author's personal toolkit. Only the author knows what a statement is meant to say and how a formalization gap in a result is best fixed. The pipeline therefore stops and asks the author whenever a statement admits more than one reading, presents every repair, in natural language and TeX symbols, as a proposal that the author can accept, decline or redirect, and leaves to the author every decision that could potentially change what the paper claims. The output is an annotated and revised version of the paper, a report of the changes, and Lean code in which each declaration is linked to the statement it formalizes. The author's toolkit grows as more papers are formalized, and authors can share their verified papers so that researchers who build on them can reuse their Lean code. By making verified papers practical to produce, PaperFormalizer aims to make research that rests on mathematical proofs more robust. PaperFormalizer runs inside a coding agent (Claude Code or Codex) and is available at https://github.com/Jiyuan-Tan/PaperFormalizer. Papers with Lean code shared by users are available at https://paperformalizer.org.