# Definition Grounding in Theory-Level Auto-formalization

arXiv: https://arxiv.org/abs/2610.19223 · HTML: https://mlsanity.com/paper/2610.19223/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 20 of its 73 references that are in the map.
- First posted on arXiv 13 Oct 2026.

## Builds on (most cited first, 20 of 20)

- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://mlsanity.com/paper/2408.03350/) (2024)
- [Reliable Evaluation and Benchmarks for Statement Autoformalization](https://mlsanity.com/paper/2406.07222/) (2024)
- [SlopCodeBench: Benchmarking How Coding Agents Degrade Over Long-Horizon Iterative Tasks](https://mlsanity.com/paper/2603.24755/) (2026)
- [SWE-CI: Evaluating Agent Capabilities in Maintaining Codebases via Continuous Integration](https://mlsanity.com/paper/2603.03823/) (2026)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [MaintainCoder: Maintainable Code Generation Under Dynamic Requirements](https://mlsanity.com/paper/2503.24260/) (2025)
- [Optimal Mixing of Glauber Dynamics: Entropy Factorization via High-Dimensional Expansion](https://mlsanity.com/paper/2011.02075/) (2020)
- [Formalizing Mathematics at Scale](https://mlsanity.com/paper/2605.29955/) (2026)
- [EvoCode-Bench: Evaluating Coding Agents in Multi-Turn Iterative Interactions](https://mlsanity.com/paper/2605.24110/) (2026)
- [Automatic Textbook Formalization](https://mlsanity.com/paper/2604.03071/) (2026)
- [APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries](https://mlsanity.com/paper/2504.19110/) (2025)
- [MathAtlas: A Benchmark for Autoformalization in the Wild](https://mlsanity.com/paper/2605.14061/) (2026)
- [Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization](https://mlsanity.com/paper/2606.13925/) (2026)
- [Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases](https://mlsanity.com/paper/2607.13292/) (2026)
- [Is Agent Code Less Maintainable Than Human Code?](https://mlsanity.com/paper/2606.21804/) (2026)
- [Random Reed-Solomon Codes Achieve List-Decoding Capacity With Linear-Sized Alphabets](https://mlsanity.com/paper/2304.09445/) (2023)
- [MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries](https://mlsanity.com/paper/2605.07147/) (2026)

## Abstract (arXiv)

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.