LeanInfoTheory builds a reusable finite-information-theory layer on mathlib, informed by existing formal libraries and the needs of downstream theorem-proving projects.

mathlib

The project is intentionally mathlib-based. It reuses mathlib PMFs, finite types, real analysis, products of measures, Markov kernels, PMF.toMeasure, binary and q-ary entropy, KL divergence, and coding-theory anchors such as Kraft-McMillan.

PMF documentation Binary and q-ary entropy KL divergence KL chain rules Kraft-McMillan

PFR Formalization

The Lean PFR project is an important reference for entropy and mutual information in a serious formalization. LeanInfoTheory keeps the first project layer finite and PMF-oriented, while auditing PFR and mathlib APIs before adding more general measure-theoretic layers.

PFR repository PFR project website PFR blueprint

Rocq Infotheo

Rocq's Infotheo library is a useful comparison point for finite distributions, conditional distributions, and textbook-style information measures. LeanInfoTheory follows Lean and mathlib naming and typeclass conventions first, but uses Infotheo as a sanity check for whether definitions can scale to larger theorem families.

Infotheo repository Rocq package page Information-theory sources

PSITIP and oXitip

PSITIP and oXitip are relevant prior art for entropy-inequality search. Their search and import workflows may inform separate downstream applications, but are not part of LeanInfoTheory's public library surface.

PSITIP repository oXitip oXitip help AITIP repository

Textbook Anchors

The near-term mathematical path is closest to the finite discrete foundations in Cover and Thomas, El Gamal and Kim, Yeung, and Polyanskiy and Wu. The project does not try to mirror a textbook line by line; it follows mathlib-compatible definitions and then records which textbook statements have been formalized.

Comparison

Reference Main role Relationship to LeanInfoTheory
mathlib General Lean foundation for PMFs, measures, real analysis, KL divergence, binary/q-ary entropy, and coding anchors. LeanInfoTheory reuses these APIs directly and adds a finite PMF-based Shannon layer rather than defining a local probability model.
PFR formalization Large Lean formalization where Shannon entropy methods are part of serious additive-combinatorics infrastructure. LeanInfoTheory treats PFR as a guide for scalable semantic bridge design, while keeping its first public layer finite and information-theorist-facing.
Rocq Infotheo Mature Rocq library for discrete probabilities, information theory, and linear error-correcting codes. LeanInfoTheory follows Lean/mathlib conventions first, but uses Infotheo as a sanity check for finite-distribution and conditional-distribution API shape.
PSITIP, oXitip, AITIP External tools for searching, checking, proving, or disproving information inequalities. These tools are relevant to downstream automation and certificate-checking applications built on reusable information-theory results.
Textbooks Mathematical reference points for finite entropy, conditional entropy, mutual information, KL divergence, and network converses. LeanInfoTheory does not mirror a textbook line by line. It uses mathlib-compatible definitions and records checked textbook-style statements on the theorem highlights page.

What This Project Adds

LeanInfoTheory currently adds a finite PMF-based Shannon layer, semantic bridges to expected self-information and KL divergence, and reusable APIs for channels, finite families, Fano inequalities, Markov structure, data processing, and sufficiency.