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

arXiv: https://arxiv.org/abs/2609.10579 · HTML: https://mlsanity.com/paper/2609.10579/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 13 references that are in the map.
- First posted on arXiv 5 Sep 2026.

## Builds on (most cited first, 5 of 5)

- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Towards a Mathematics Formalisation Assistant using Large Language Models](https://mlsanity.com/paper/2211.07524/) (2022)
- [Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory](https://mlsanity.com/paper/2607.09632/) (2026)
- [Formalizing building-up constructions of self-dual codes through isotropic lines in Lean](https://mlsanity.com/paper/2604.08485/) (2026)

## Abstract (arXiv)

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/n4codelean.