Dong and Yang's 27-page classification of optimal finite-length (n,4) binary block codes for binary symmetric channels is long and complex, making human verification difficult. The goal is a machine-checked correctness guarantee for its classification theorems (Theorems 1-5).

The paper's LaTeX source is fed to AI coding agents (OpenAI Codex models) to autoformalize the proofs in Lean 4, building on Mathlib for finite types, big sums, parity, and real arithmetic. Codes are modeled with columns as the primary object (Code n = Fin n → Column). Parallel AI agents discharge the generated sorry statements, followed by a human-guided axiom audit ensuring dependence only on Lean's standard base axioms (propext, Quot.sound, Classical.choice) and elimination of native_decide.

The resulting library is sorry-free and axiom-audited, totaling 37,561 lines across fourteen modules, with lake build succeeding and every headline theorem proved. Formalization exposed imprecise hypotheses and gaps in the original paper's proofs, leading to strengthened statements and a catalogue of discrepancies.