A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs
math.HO, cs.AI, cs.IT, math.IT
Submitted: 2026-09-05
Updated: 2026-09-05
Code: https://github.com/shhyang/n4code
License: http://creativecommons.org/licenses/by-nc-sa/4.0/
The gist: 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.
Terminology
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 https://github.com/shhyang/n4code lean.
Related papers
- A unified interpretation of probability
- Remembering Solomon Marcus
- Math for AI safety: an invitation for mathematicians
- LLAMA LIMA: A Living Meta-Analysis on the Effects of Generative AI on Learning Mathematics
- If you can distinguish, you can express: Galois theory, Stone--Weierstrass, machine learning, and linguistics
- Explanations, Prompts, and Formalizations: Arguments for New Norms in LLM-Enabled Mathematical Research