Definition Grounding in Theory-Level Auto-formalization

Leyan Pan; Christian Szegedy; Frederick Rajasekaran; Robi Bhattacharjee; Gregory Constantine; Wenke Lee

cs.AIOct 13, 2026

Definition Grounding in Theory-Level Auto-formalization

Authors: Leyan Pan, Christian Szegedy, Frederick Rajasekaran, Robi Bhattacharjee, Gregory Constantine, Wenke Lee

Organizations: Georgia Institute of Technology · AletheAI · Stanford University

Abstract

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$	$S_{1}$	$S_{2}$	$S_{3}$	$S_{4}$	$S_{5}$
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

S_{1},\dots,S_{5}

of every theory in ReuseBench.

Source
	Witness rate (%)					Full pass
Model	$S_{1}$	$S_{2}$	$S_{3}$	$S_{4}$	$S_{5}$	rate (%)
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

S_{1},\dots,S_{5}

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(\dot{D})=\mathit{True}

, i.e., that are fully compatible.

	Baseline	$D$ ( $J_{0}$ )	$+S_{1}$ ( $J_{1}$ )	$+S_{2}$ ( $J_{2}$ )	$+S_{3}$ ( $J_{3}$ )	$+S_{4}$ ( $J_{4}$ )
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

\mathit{True}

) and of the judges

J_{0},\dots,J_{4}

against the compatibility label

L(\dot{D})

, over all 8 theories.

Figure 1: Precision-recall curves of the judges

J_{0},\dots,J_{4}

against the compatibility label

L(\dot{D})

, over all 8 theories, thresholding the number of accepting calls out of 5.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Theory	Source	Layers	Copy used	License
Markov chain mixing times	Levin and Peres (2017)	$D$ , $S_{1}$ – $S_{5}$	Authors’ PDF (2nd ed.)	In copyright; free PDF from the authors
	Diaconis and Shahshahani (1981)	$S_{4}$	–	©Springer-Verlag
	Bayer and Diaconis (1992)	$S_{4}$	–	©IMS
	Cryan et al. (2021)	$S_{5}$	arXiv:1903.06081v4	arXiv non-exclusive license
	Ding et al. (2010)	$S_{5}$	arXiv:0801.2625v4	arXiv non-exclusive license
	Basu et al. (2017)	$S_{5}$	arXiv:1409.3250v4	arXiv non-exclusive license

Appendix

Table 4: Detailed source and license of each theory we collected

Autoformalization

Autoformalization converts natural-language mathematics, proofs, and specifications into machine-checkable formal languages.

See all 116 papers

Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization
Oct 14, 2026Anna Mei, Michael R. DouglasFormal Verification Autoformalization
Harvard University · CMSA, Harvard University and AletheAI, Inc
Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
Jun 30, 2026Arshia Soltani Moakhar, Iman Gholami, Max Springer +2Multi-Agent LLM Systems Automated Theorem Proving
PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
Oct 22, 2026Jiyuan Tan, Jose Blanchet, Vasilis SyrgkanisAutoformalization Formal Verification
Stanford University

Oct 14, 2026J/K move · Enter open · S save

Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

Anna Mei, Michael R. Douglas

Harvard University · CMSA, Harvard University and AletheAI, Inc

Formal Verification Autoformalization LLM-as-a-Judge

Open paper AskPDF arXiv

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.

Abstract

Autoformalization

Explore similar work

Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean