Aligning Information Theory and Formal Verification: A Lean Formalization of Rate-Distortion Theory

Fubin Yan, Ruxuan Dong, Ruoxuan Shi +2

Large language models have recently demonstrated an ability to generate substantial mathematical proofs and formalizations, including machine-checked arguments for major open probl…