Information theory in Lean: the DPI

Abstract: The Data Processing Inequality (DPI) is a cornerstone of information theory, expressing the principle that information cannot be created through processing.

In this talk, I will present the formalization of information-theoretic results carried out by Rémy Degenne and myself using the Lean 4 theorem prover. The focus will be on the formalization of information divergences—particularly f-divergences—and their associated Data Processing Inequality (DPI), along with their connection to the framework of hypothesis testing. I will also discuss the key challenges and design decisions faced during the project.

logic in computer sciencemathematical softwareinformation theory

Audience: researchers in the discipline

( video )

---

Lean Together 2025

Series comments: Most of the talks from the conference are available on YouTube: www.youtube.com/watch?v=ZPPDktjL1Lw&list=PLlF-CfQhukNlzXdQvu1SVt9vcD4--fLlg

---