Definition Grounding in Theory-Level Auto-formalization
Leyan Pan, Christian Szegedy, Frederick Rajasekaran, Robi Bhattacharjee, Gregory Constantine, Wenke Lee
cs.AI
Oct 13, 2026 · v1
TL;DR
Introduces ReuseBench, in which LLM agents formalize definitions and layered statements of textbook theories in Lean 4 on top of Mathlib, and evaluates definition reusability.
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.
Problem
LLM auto-formalization systems produce Lean code quickly, but their formalized definitions are often unusable for downstream statements. This makes theory-level formalization libraries hard to build on.
Approach
The authors propose definition grounding, where definition formalizations are continuously judged and revised. They curate ReuseBench: 8 theories from textbooks, each with core definitions followed by up to 5 layers of increasingly advanced statements, formalized from an empty Mathlib-based project. Definition sets written by frontier models are tested by having a canonical agent formalize the downstream layers. They also study LLM judges that predict compatibility, with and without first formalizing basic downstream statements.
Results
Only 25%-50% of definition sets written from source text are compatible with all later statements. Clarifying the informal definitions raises the rate to 77.5% averaged over models. Stating a small set of basic properties without proofs improves judge accuracy from 0.65 to 0.85, at about 11% of the definition formalization cost.
| Model | Source | Cleaned |
|---|
| GPT 6 Astra | 43.8 | 81.2 |
| Claude Fable 5.1 | 50.0 | 100.0 |
| Claude Opus 5 | 50.0 | 87.5 |
| All models | 40.0 | 77.5 |
Full pass rate (%) of definition formalizations from source text vs. cleaned statements
