Aligning Information Theory and Formal Verification: A Lean Formalization of Rate-Distortion Theory
Abstract
Large language models have recently demonstrated an ability to generate substantial mathematical proofs and formalizations, including machine-checked arguments for major open problems and classical theorems. These developments highlight a growing workflow in which AI systems search for proofs while proof assistants certify their correctness. Within information theory, however, formalized libraries remain limited, and existing formalized theorems focus almost exclusively on Shannon's foundational lossless theorems. This paper presents the first Lean formalization of core components of rate-distortion theory, a central framework for lossy compression and modern machine-learning analysis. We identify the alignment challenges that arise when translating information-theoretic definitions, such as distortion measures, typicality and achievability, into a proof-assistant setting, and we develop a reusable library of definitions and lemmas faithful to textbook conventions. Our formalization provides a foundation for future AI-assisted proofs in information theory and enables subsequent mechanized developments to build on a coherent, verified infrastructure rather than generating long proofs from scratch.
Related
- A Self-Coupling Gaussian Extremal Inequality for Information-Constrained Optimal Transport with Applications to Rate-Distortion-Perception
- An Overview of Rate-Distortion-Perception Theory
- Generative Rate-Distortion-Perception Theory on Riemannian Manifolds
- Rate-Distortion Theory of Gaussian Mixtures via Posterior Label Sampling
- Verification with Transfer: Exact Information Frontiers and Their Price in Calls
BibTeX
@misc{yan2026aligning,
title = {{Aligning Information Theory and Formal Verification: A Lean Formalization of Rate-Distortion Theory}},
author = {Fubin Yan and Ruxuan Dong and Ruoxuan Shi and Duolei Wang and Kenneth W. Shum},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.22404},
eprint = {2610.22404},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.22404},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Aligning Information Theory and Formal Verification: A Lean Formalization of Rate-Distortion Theory
AU - Fubin Yan
AU - Ruxuan Dong
AU - Ruoxuan Shi
AU - Duolei Wang
AU - Kenneth W. Shum
PY - 2026
DA - 2026/10/14
PB - arXiv
DO - 10.48550/arxiv.2610.22404
UR - https://arxiv.org/abs/2610.22404
AB - Large language models have recently demonstrated an ability to generate substantial mathematical proofs and formalizations, including machine-checked arguments for major open problems and classical theorems. These developments highlight a growing workflow in which AI systems search for proofs while proof assistants certify their correctness. Within information theory, however, formalized libraries remain limited, and existing formalized theorems focus almost exclusively on Shannon's foundational lossless theorems. This paper presents the first Lean formalization of core components of rate-distortion theory, a central framework for lossy compression and modern machine-learning analysis. We identify the alignment challenges that arise when translating information-theoretic definitions, such as distortion measures, typicality and achievability, into a proof-assistant setting, and we develop a reusable library of definitions and lemmas faithful to textbook conventions. Our formalization provides a foundation for future AI-assisted proofs in information theory and enables subsequent mechanized developments to build on a coherent, verified infrastructure rather than generating long proofs from scratch.
ER -