A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs

Abstract:We present a machine-checked Lean~4 formalization of Dong and Yang's classification of optimal finite-length $(n,4)$ binary block codes for binary symmetric channels. The formalization was developed mainly by feeding the paper's proofs to an AI tool. To establish correctness, the authors verified the main theorem statements in Lean and the accepted axioms. This note discusses the corrections and simplifications made to the AI-generated formalization, and records discrepancies found in the paper during the formalization. The Lean code is available at this https URL.

History and Overview (math.HO); Artificial Intelligence (cs.AI); Information Theory (cs.IT)

arXiv:2609.10579 [math.HO]

(or arXiv:2609.10579v1 [math.HO] for this version)

https://doi.org/10.48550/arXiv.2609.10579 Focus to learn more arXiv-issued DOI via DataCite

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.