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.