We released N4Code, a Lean 4 +
mathlib formalization that machine-checks the classification theorems of our
paper On Optimal Finite-Length Block Codes of Size Four for Binary Symmetric
Channels (IEEE Transactions on Information Theory, 2025): for every
blocklength n and crossover probability ε, an optimal (n, 4) binary code
exists that is equivalent to a linear or Class-I code, and for n > 3 every
optimal code is equivalent to a linear, Class-I, or Class-II code.
The proof scripts were developed with substantial assistance from AI coding agents; all the main theorem statements and definitions were checked by us, and every proof is machine-checked by the Lean 4 kernel. Archived with DOI: 10.5281/zenodo.22253544.