Skip to content
DraconiticResearch
Search Sources API
203,234 studies31 sourcesUpdated 31 min ago
PreprintCC BY-NC-SA 4.0arXiv

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

  • Shenghao Yang
  • Yanyan Dong
Open at sourcePDFDOICite

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

  1. A Machine-Checked Proof that Gardam's Ã2 Lattice Does Not Have Unique Products
    Ibrahim Mian, Shayaan Siddique
    arXivPreprintCC BY 4.0Full textAlgebra & number theoryarXiv
  2. A Diverging History Clock Is Not a Blow-up Proof: Lean-Checked Lemmas Showing Why a Section 10 Navier-Stokes Argument Does Not Certify Fefferman (C) or (D)
    Benjamin Frohman
    Zenodo (CERN European Organization for Nuclear Research)PreprintLicence not stated8 citedGeneral mathematicsOpenAlex
  3. Benchmarking Classical Machine Learning and Deep Learning Models on the Cleveland Heart Disease Binary Classification Dataset
    Ajimah Nnabueze Edmund, Ikiomoye Douglas Emmanuel, Esenogho Ebenezer
    Journal of Information Systems and InformaticsPeer-reviewedCC BYFull textGeneral mathematicsDOAJ
  4. The triangular lattice minimises the planar Yukawa energy at every density and for every finite mixture of screening lengths: kernel-checked corollaries of planar universal optimality, a human proof, and an exact-potential CVODE consistency study
    Xavier Callens
    Zenodo (CERN European Organization for Nuclear Research)PreprintCC BY11 citedNumerical analysis & scientific computingOpenAlex
  5. A proof of the Braun-Etzion-Vardy bound for binary subspace codes
    Srikanth B. Pai
    arXivPreprintarXiv licenceFull textCombinatorics & discrete mathematicsarXiv

Cite

BibTeXRIS
BibTeX
@misc{yang2026machinechecked,
  title = {{A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs}},
  author = {Shenghao Yang and Yanyan Dong},
  howpublished = {arXiv},
  year = {2026},
  month = sep,
  doi = {10.48550/arxiv.2609.10579},
  eprint = {2609.10579},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2609.10579},
  note = {CC BY-NC-SA 4.0},
}
RIS
TY  - UNPB
TI  - A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs
AU  - Shenghao Yang
AU  - Yanyan Dong
PY  - 2026
DA  - 2026/09/05
PB  - arXiv
DO  - 10.48550/arxiv.2609.10579
UR  - https://arxiv.org/abs/2609.10579
AB  - 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.
ER  -