This is an unofficial reimagining of the Archive of Formal Proofs
Source Coding Theoremby Quentin Hibon and Lawrence C. Paulson