Some Coding Theory In Lean

This project contains some formalized coding theory, written in Lean 3. See the accompanying report for more details.

Setup & Installation

The best way to read this code is using a local installation of Lean. See the Lean Community Guide for instructions.

Once installed, run

leanpkg configure
leanproject build
leanproject get-mathlib-cache

in this directory to setup the project.

binary.lean
- Contains fundamental definitions: bits, binary words, binary word matrices.
- Namespaces: B for bits, BW for binary words, BWM for binary word matrices.
hamming.lean
- Contains definitions of Hamming distance and weight and proofs of basic properties.
- Namespace: hamming so that one can write hamming.distance or hamming.weight.
- Also includes notation for these functions: d(x,y) and wt(x).
binary_codes.lean
- Contains the definition of a binary code and the main proofs of the project, see comments in file for more details.
- All contained in namespace binary_code.
linear_binary_code.lean
- Defines an extension of binary codes, linear binary codes.
- Also contains an example linear code, the Hamming(7,4) code, and contains proofs of some basic properties of this code.
syndrome_decoding.lean
- Contains a formalization of the Hamming(7,4) code and a proof that syndrome decoding is a 1-error correcting decoding procedure for this code.
qary_codes_example.lean
- Contains examples of the distance and weight functions defined for q-ary words (vectors) and some sample proofs.
hamcode_widget.lean
- Contains an interactive widget showing the encoding/decoding procedure for the Hamming(7,4) code.
- See the mathlib documentation on widgets for more information.