A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs
math.HO · cs.AI · cs.IT
Quick verdict
Credible, axiom-audited Lean 4 formalization (37.6k lines, ~48h mostly AI) of the Dong–Yang (n,4) BSC code classification; it documents real gaps in the paper.
Summary
This note reports a complete Lean 4 formalization of Dong and Yang's classification of optimal finite-length (n,4) binary codes for the binary symmetric channel, published in IEEE Trans. Inf. Theory (2025). The authors fed the paper's LaTeX source to OpenAI Codex (deepseek-v4-flash, then deepseek-v4-pro); AI agents discharged all sorry placeholders in roughly 48 hours with light human intervention, yielding 14 modules and 37,561 lines. The main methodological contribution is an audit: headline theorem statements are verified against the paper, all 215 native_decide declarations are replaced with kernel-checked decide so only Lean's standard axioms (propext, Classical.choice, Quot.sound) remain, and this is enforced automatically via AxiomCheck.lean and scripts/axioms_check.sh. Formalization also exposed genuine defects in the published proofs: a stated-but-unproved type-invariance claim, a gap in the Corollary 10 column-change argument, missing steps in the Theorem 3 and 4 proofs, a class-labeling error in Lemma 15, and vacuous or incorrect cases in Theorem 16; the Lean development closes several of these with stronger universal strict-domination statements. Limitations: the development deliberately avoids mathlib's coding-theory library, limiting reuse; Class-I/II/III separation is established only through column-weight parity; and the claim that AI-assisted formalization needs little human expertise rests on a single case study. The code is public on GitHub.
Review complete
Assessment at a glance
4
risk flags identified
● high 0
● medium 2
● low 2
5 strengths · 5 weaknesses · 5 author questions
AI text signal = Binoculars zero-shot detector score over 20 sampled passages (Fast-DetectGPT co-reported) — absence does not prove human authorship, and a flag does not imply misconduct.
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- All five classification theorems of Dong–Yang for optimal (n,4) binary codes on BSCs are proved in Lean 4, sorry-free, with dependencies only on propext, Quot.sound, and Classical.choice.
- All 215 native_decide declarations were replaced with kernel-checked decide, so the Lean compiler/runtime is not part of the trusted computing base.
- The formalization uncovered concrete defects in the published paper: an unproved type-invariance claim, a gap in Corollary 10's argument, missing steps in Theorems 3–4, mislabeled classes in Lemma 15, and vacuous/incorrect cases in Theorem 16.
- AI agents (OpenAI Codex with deepseek-v4-flash, later deepseek-v4-pro) discharged the proofs in about 48 hours with only light human intervention, producing 14 modules totalling 37,561 lines.
Strengths
Trust audit exceeds community norms
§3.1 goes beyond a sorry-free build: #print axioms on every headline theorem, an allowlist of only propext/Quot.sound/Classical.choice enforced by scripts/axioms_check.sh, and all 215 native_decide declarations (Table 3; Reduction 91, FiniteN 33, Nbig 24…) rewritten to kernel-checked decide, removing the Lean runtime from the trusted computing base.
Formalization returned real value to the original field
§4/Table 4 documents concrete defects in the published IEEE TIT paper: the unproved type-invariance claim (§4.1), the Corollary 10 gap where Theorem 8 covers only w(c3⊕c4) even (§4.2), missing steps in Theorems 3–4 including the 'equivalent to Class-II' claim (§4.3), the 'Class-II-b'→'Class-III-b' relabeling in Lemma 15, and Theorem 16's vacuous n=3 clause plus the n=2 impossibility argument (§4.4), each closed with explicit Lean lemmas.
Strengthened, cleaner theorem statements
Transparent AI workflow with auditable markers
Reusable generic core
Weaknesses
Statement fidelity is self-audited with authorship overlap
Deliberate isolation from mathlib's coding theory
Overgeneralized conclusion from n=1
Efficiency claims lack measurement
Upstream errata status unaddressed
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
Report preview
Scope & Claims
This is a formalization report, not new coding theory: it documents a Lean 4 machine-checked proof of Theorems 1–5 of Dong & Yang (IEEE Trans. Inf. Theory 71(1):138–166, 2025), which classify optimal finite-length (n,4) binary codes for the BSC. The headline results (§2.2): (T1) for every n≥2 and ε∈(0,1/2) an optimal code exists that is linear or Class-I; (T2) linear optima classified by n mod 3; (T3) for n>3 every optimal code is equivalent to a linear, Class-I or Class-II code; (T4) under a Class-I replacement condition all optima are equivalent to linear codes; (T5) full classification for 2≤n≤8. Beyond reproduction, the authors prove strengthened universal strict-domination versions and catalogue discrepancies in the printed proofs (Table 4).
The remaining sections cover Methodology Assessment, Statistical Evidence, Results & Reproducibility, Limitations & Risks, and Verdict & Recommendations.
- All 5 strengths & 5 weaknesses, analyzed in detail
- 4 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
What does this paper formalize?
It formalizes, in the Lean 4 proof assistant, the five classification theorems from Dong and Yang's IEEE Trans. Inf. Theory (2025) paper, which determine which binary codes of length n with exactly four codewords maximize correct-decoding probability on a binary symmetric channel, for all blocklengths and for 2 ≤ n ≤ 8 in full detail.
Did AI write the Lean proofs?
Largely yes: the paper's LaTeX source was fed to OpenAI Codex (deepseek-v4-flash, later deepseek-v4-pro), and AI agents removed all proof placeholders in about 48 hours. The authors then audited the theorem statements and axiom dependencies and replaced all 215 native_decide uses with kernel-checked decide.
Were errors found in the original Dong–Yang paper?
Yes. The formalization uncovered an unproved type-invariance claim, a gap in the Corollary 10 column-change argument, missing steps in the Theorem 3 and 4 proofs, a 'Class-II-b' label that should read 'Class-III-b' in Lemma 15, and vacuous or incorrect cases in Theorem 16's proof; the Lean version proves corrected, often stronger statements.
Where is the Lean code and how can I verify it?
At github.com/shhyang/n4code_lean: fourteen modules totalling 37,561 lines, including AxiomCheck.lean and scripts/axioms_check.sh, which mechanically verify that every headline theorem depends only on Lean's three standard axioms (propext, Quot.sound, Classical.choice).
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- The provided text is complete through the reference list; the GitHub repository and its cited line ranges are external to it, so statement fidelity was assessed from the authors' descriptions rather than the Lean sources.
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.