AI-Assisted Lean 4 Formalization of Binary Code Classification

Authors used AI tools to facilitate a Lean 4 machine-checked proof of the Dong-Yang classification for optimal (n,4) binary block codes. The process involved correcting and simplifying AI-generated formalizations to verify theorem statements against original axioms.