ECC

A Lean 4 project depending on cslib and mathlib (transitively).

Goal is to formalize Error Correction Codes in Lean.

Prereqs

You need elan installed.

Building

git clone https://github.com/wurtylex/Lean-Formalization-of-Error-Correction-Codes-
cd Lean-Formalization-of-Error-Correction-Codes-
lake exe cache get
lake build

References

The primary reference for this project is:

• Venkatesan Guruswami, Atri Rudra, and Madhu Sudan, Essential Coding Theory. PDF

Unless stated otherwise, definitions and statements follow the conventions of that book.

Project Layout

TODO