Source-linked AI summary
A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs
Shenghao Yang, Yanyan Dong
TL;DR
Long mathematical proofs have traditionally demanded substantial verification effort, motivating machine-checked formalization. This paper formalizes Dong and Yang’s optimal (n, 4) code classification in Lean, audits its statements, and identifies a sharper universal domination result.
Problem
Substantial mathematical proofs are difficult to verify by hand, while machine-checked developments have historically required years of effort and specialized expertise.
Source: §1 · p. 2Method
The authors formalize Dong and Yang’s classification in Lean and compare the paper’s theorem statements with the formalized results, including stronger domination statements for Theorems 3–5.
Source: §4.3 · p. 17Results
For n ≥ 2, an optimal code exists that is linear or Class-I; the formalization also sharpens Theorem 3 to show that any code outside the three classes has another code strictly better at every crossover probability.
Source: §2.2.1 · p. 8, §2.2.3 · p. 10Takeaways & Limitations
The formalization yields a generic core independent of this specific (n, 4) classification problem.
Source: §3 · p. 11For cases listing multiple optima, the paper’s domination wording requires reading a competitor as non-equivalent to every listed optimum.
Source: §2.2.2 · p. 9
Abstract
from arXiv · showhide
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.
1 Introduction
The introduction frames machine-checked formalization as a route to correctness and reproducibility, while noting the historical effort required for substantial proofs. It places this work within coding-theory formalization and states conventions for reading its Lean discussion.
1 Introduction
- Machine-checked formalization promises correctness and reproducibility, but substantial developments have historically required years of dedicated effort.The introduction cites the multi-year, multi-person Flyspeck and Feit–Thompson formalizations as examples.Source: §1 · p. 2
- Existing coding-theory formalizations cover foundational, classical, and structural results rather than end-to-end formalizations of contemporary research papers.Examples include Coq’s infotheo library, Lean’s InformationTheory namespace, and projects on covering codes, self-dual constructions, Reed–Solomon codes, and quantum Shannon theory.Source: §1 · p. 2
1.2 Conventions
- The note cites theorems, lemmas, corollaries, and displayed equations by their numbers in.It uses the paper’s codeword indexing and Lean’s row0–row3 indexing interchangeably.Source: §1.2 · p. 4
2 Formalization Design of Binary Codes
This section introduces the Lean formulation of the code model and the statements used to compare its formalized theorems with the paper. It also explains Lean’s proof model and the development’s mathlib infrastructure.
2 Formalization Design of Binary Codes
- Section 2.1 introduces the code model, and Section 2.2 presents Lean statements of Theorems 1–5 for comparison with the paper.Source: §2 · p. 5
- Lean represents mathematical objects and propositions as types, with proofs as programs whose types are the theorem statements.Lean’s trusted kernel checks the resulting typing judgments.Source: §2 · p. 5
- The development uses mathlib for finite types, finite sums, parity, and real arithmetic.The project is organized in the N4Code namespace.Source: §2 · p. 5
2.1 Binary Codes in Lean
The formalization models four-word binary codes through their columns, defines decoding performance and universal comparisons, and represents equivalence and code classes through column operations and counts. It permits repeated rows in intermediate Lean objects while proving that optimal codes have distinct rows.
2.1 Binary Codes in Lean
- A code is optimal when it maximizes the correct-decoding probability under maximum-likelihood decoding for a BSC with crossover probability ε.Source: §2.1 · p. 5
2.1.1 Basic Definitions of Codes
- The formalization takes the columns of the 4 × n codeword matrix as its primary objects.A Code n is given by n columns, each a four-bit column indexed by Fin 4.Source: §2.1.1 · p. 5
- Code n allows repeated rows, unlike the paper’s four-distinct-word code, and records row distinctness separately.The enlarged space simplifies intermediate column transformations; repeated-row matrices are universally strictly dominated, so optimal Lean codes have distinct rows.Source: §2.1.1 · p. 5, §2.1.2 · p. 7
2.1.2 Performance of Codes
- The formalization defines code performance as an average correct-decoding probability and compares codes either at fixed ε or universally over 0 < ε < 1/2.UniversalBetter and UniversalStrictBetter express pointwise non-strict and strict comparisons, respectively.Source: §2.1.2 · pp. 6–7
2.1.3 Equivalence and Code Classes
- Code equivalence permits row permutations, column permutations, and bit flips in columns, and equivalent codes have the same λ_C.Source: §2.1.3 · p. 7
- Linear, Class-I, Class-II, and Class-III codes are characterized through column-type counts and their stated parity or count patterns.The canonical linear representative with counts |3| = n3, |5| = n5, and |6| = n6 is linearCode n3 n5 n6.Source: §2.1.3 · pp. 7–8
2.2 Statements of Main Theorems
The five theorems classify optimal (n, 4) codes through linear and nonlinear classes, with special results for linear codes and blocklengths 2–8. The formalization sharpens the universal comparison statement and records an imprecision in the paper’s description of multiple linear optima.
2.2.1 Theorem 1 (optimal_in_linear_or_class1)
- For every n ≥ 2 and ε ∈ (0, 1/2), at least one optimal code is linear or Class-I.Source: §2.2.1 · p. 8
2.2.2 Theorem 2 (linear_opt_*)
- By n mod 3, Theorem 2 lists optimal linear codes for each residue class and states strict superiority over non-equivalent competitors.When several optima are listed, they can have equal λ; the domination claim applies to competitors non-equivalent to every listed optimum.Source: §2.2.2 · p. 9
2.2.3 Theorem 3 (universal_strict_better_of_not_class)
- For n > 3, the formalization sharpens Theorem 3: any code outside the three classes has another code strictly better at every crossover probability.The paper states that all optimal codes are among the optimal linear, Class-I, Class-II, and equivalent codes.Source: §2.2.3 · pp. 9–10
2.2.4 Theorem 4 (universal_strict_better_of_not_linear)
- Under Theorem 4’s Class-I replacement condition, a code not equivalent to a linear code has a universally strictly better code.The theorem uses a one-column change, replacing a column with a type of minimal count among 3, 5, and 6, with ties broken in that order.Source: §2.2.4 · p. 10
2.2.5 Theorem 5 (optimal_codes_small_n)
- For 4 ≤ n ≤ 8, verifying Theorem 4’s hypothesis yields a universally strictly better code for each code not equivalent to a linear code; Theorem 4 does not cover n = 2.Source: §2.2.5 · p. 11
- At n = 3, codes outside five listed representatives have a universally strictly better code, while each representative is universally optimal.The five representatives are code135, code136, CA, linearCode 1 1 1, and linearCode 1 2 0.Source: §2.2.5 · p. 11
3 Proof Formalization Development
AI-assisted proof development produced a sorry-free Lean library, followed by an axiom audit and a simplification pass that extracted reusable infrastructure. The work also separates generic machinery from the classification-specific components.
3 Proof Formalization Development
- All sorrys were discharged in about 48 hours with light human intervention, yielding a 37,561-line library whose headline theorems build successfully.The code is organized across fourteen modules.Source: §3 · p. 11
3.1.1 Trusted Axioms
- The authors audited theorem dependencies as well as proof completion, requiring headline theorems to use only Lean’s standard base axioms.The audit tool checks each theorem’s axioms against an allowlist and rejects unapproved dependencies such as sorryAx.Source: §3 · p. 11, §3.1.1 · p. 12
3.1.2 From native_decide to decide
- Replacing native_decide with decide moved finite checks from compiled native execution and its trust axioms to kernel reduction.The finite checks were small enough for kernel computation, with a higher recursion-depth setting used where needed.Source: §3 · p. 11, §3.1.2 · p. 12
- The earlier draft had 215 native_decide-bearing declarations, and Table 3 records their distribution by module before replacement.The retained audit markers record the group, block length, and check date; the authors checked that each marker matched its declaration.Source: §3.1.2 · p. 13, Table 3 · p. 13
3.2 Simplifications
- The simplification pass replaced repeated arguments with shared lemmas for row distances, Class-I swap hypotheses, and involutive type-count transports.General count-replacement helpers also made several specialized cases short corollaries.Source: §3.2 · pp. 13–14
3.3 Reusable Generic Core
- The generic tier collects code and Hamming-distance machinery, equivalence transport, BSC comparisons, and reusable counting and grouping facts.These foundations are independent of Class-I, Class-II, and Class-III assumptions.Source: §3.3 · p. 14
- The 4-column Class-I components remain problem-specific but are factored for reuse, and the classification modules build on the generic tier.This replaces repeated ad-hoc case analyses with shared components.Source: §3.3 · p. 15
- The authors expect the generic infrastructure, including distance-distribution and equivalence-invariance machinery, to support future information-theory formalizations.A machine-checked paper-to-Lean dictionary and consistency tooling help keep the correspondence auditable.Source: §3.3 · p. 15
4 Notable Discrepancies
The formalization exposed places where the paper’s equivalence arguments, column-change proofs, and theorem statements needed sharper hypotheses or explicit steps. Lean supplies proofs for gaps and records corrections to several printed claims.
4.1 Code Types Under Equivalence
- Lean uses parity of column Hamming weights to separate linear codes from Class-I, Class-II, and Class-III, but this invariant does not separate those three nonlinear classes.The paper’s multiset-invariance argument is not formalized directly.Source: §4.1 · p. 16
4.2 Gaps in the Column-Change Arguments
- For Corollary 10, Lean closes the column-change gap in the two even-row-pair cases left to a remark after Theorem 8.One case uses a 1-to-5 flip; the other first swaps rows to reduce to that case while preserving the relevant total counts.Source: §4.2 · p. 16
4.3 Proofs of Theorems 3 and 4
- Lean makes the Theorem 3 Class-III claim precise: exactly one of the type-5 and type-6 counts is zero in the specified linear image.If both were zero, the image would contain only type-3 columns.Source: §4.3 · p. 16
- In Lemma 15, two cases labeled Class-II-b should instead be labeled Class-III-b; the lemma’s conclusion is unchanged.The correction follows from the cases’ |1| = 1 condition and the stated row-swap equivalence.Source: §4.3 · p. 17
- For Theorem 4’s Class-I descent, Lean constructs an equivalence to Class-II separately for each possible argmin type before applying Lemma 14.The type-5 case needs a row swap; the type-6 case uses a type relabelling realized by column flips and a row swap.Source: §4.3 · p. 17
4.4 Proof of Theorem 16
- Theorem 16’s comparison is strict when n ≠ 3 and equal when n = 3, but the equality case is vacuous for genuine codes with distinct rows.Lean’s Code type alone allows duplicate rows, so the formalized theorem adds a DistinctRows hypothesis.Source: §4.4 · p. 17
- The proof’s count-one claim for 2 ≤ n ≤ 4 should be restricted to n = 4; the n = 2 case is impossible and n = 3 is vacuous.At n = 4, the common-parity condition and total count imply |3| = |5| = |6| = 1.Source: §4.4 · p. 17
- For Theorem 16’s count-one case, Lean supplies equivalence reductions for argmin types 5 and 6 and states the Y3/Y5 criteria without parity-dependent division.The paper’s quotients are integral only under the Class-I parity condition.Source: §4.4 · pp. 17–18
5 Final Remarks
The note presents a kernel-checked Lean 4 formalization of a coding-theory proof and emphasizes auditing as part of establishing correctness. The authors report that formalization exposed proof gaps and suggest AI-assisted generalization as future work.
5 Final Remarks
- The authors present a complete, kernel-checked Lean 4 formalization of proofs from a coding-theory research paper.They emphasize that the audit is essential to establishing correctness.Source: §5 · p. 18
- Formalization provided a reproducible check, exposed imprecise or incorrect proof statements, and helped guide AI toward more accurate proofs and new results.These are the authors’ three reported lessons from the work.Source: §5 · p. 18
- Using AI to extend or generalize the finite-length code results was not explored in this note.The authors identify it as a possible direction for future research.Source: §5 · p. 18