Research
A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs
arXiv:2609.10579v1 Announce Type: cross 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 symme
arXiv:2609.10579v1 Announce Type: cross 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
- Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries
- Lean-GAP: A Dataset of Formalized Graduate Algebra Problems
- Block-Sphere Vector Quantization
Source: arXiv cs.AI | 2026-09-12