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

Shenghao Yang; Yanyan Dong

math.HOSep 12, 2026

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

Authors: Shenghao Yang, Yanyan Dong

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.

Explore similar work

Formalizing building-up constructions of self-dual codes through isotropic lines in Lean
Date pendingJae-Hyun Baek, Jon-Lark KimSource-Channel Coding Construction
Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalization
Apr 25, 2026William Feng, Ethan Lou, Aryan SharmaAutoformalization Paraphrasing
Evaluation of LLMs for Mathematical Formalization in Lean
Jun 4, 2026Tyson Klingner, Drew Bladek, Escher Crawford +6Theorem Formalization

Date pending · cs.ITJ/K move · Enter open · S save

Formalizing building-up constructions of self-dual codes through isotropic lines in Lean

Jae-Hyun Baek, Jon-Lark Kim

The purpose of this paper is two-fold. First, we show that, after a specified form isometry, the two-coordinate reduction in the binary Hilbert-symbol realization of Chinburg and Zhang is inverse to Kim's building-up construction, up to permutation equivalence. Second, for

q\equiv1\pmod4

, we develop a

q

-ary analogue of this reduction-and-extension mechanism. The identity

c^2=-1

yields the isotropic line governing the split construction. For every fixed ordered pairing of the coordinates, we obtain a universal rank-

r

boxed normal form, where

r

is the dimension of the intersection with the product of these isotropic lines. Applications include optimal self-dual

[6,3,4]

and

[8,4,4]

codes over

\mathbb F_{5}

, optimal self-dual

[8,4,5]

and

[10,5,6]

codes over

\mathbb F_{13}

, and a self-dual

[12,6,6]

code over

\mathbb F_{13}

. We also give an exact repeated boxed realization of self-dual

[18,9,8]

and

[20,10,10]

codes over

\mathbb F_{13}

, in which the split-boxed parent and its building-up child occur in one complete generator matrix. The algebraic core is formalized in Lean 4.

Source-Channel Coding Construction Kernel Hilbert Spaces

Open paper Ask about it PDF

Abstract

Explore similar work

Formalizing building-up constructions of self-dual codes through isotropic lines in Lean

Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalization

Evaluation of LLMs for Mathematical Formalization in Lean