Formalization of coding theory using lean
Manabu Hagiwara, Kyosuke Nakano, Justin Kong · International Symposium on Information Theory and its Applications · 2016
In this paper we report on work done to formalize coding theory in the Lean theorem prover, released by Microsoft Research and Carnegie Mellon University in 2015. We formalize definitions and theorems in a downloadable library named Cotoleta (COding Theory Over the LEan Theorem-proof Assistant). This is the first coding theory library for Lean. Our formalization includes new template-like structures for formalizing error-correcting systems. As examples, repetition codes and the Hamming (7,4) code are formalized using these structures. The reader is assumed to have some knowledge of information and coding theory but no formalization experience is assumed.