Dong-Yang 二元对称信道最优 (n,4) 二元码分类的机器验证证明
A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs
浏览论文内容
中文总结 AI 辅助
本文用 Lean 4 机器验证了 Dong-Yang 关于二元对称信道最优 (n,4) 二元码分类的定理，通过 AI 辅助形式化并修正了差异，代码公开。
中文摘要 AI 辅助
我们给出了 Dong 和 Yang 关于二元对称信道的最优有限长 $(n,4)$ 二元分组码分类的 Lean~4 机器验证形式化。该形式化主要通过将论文的证明输入 AI 工具而开发。为确立正确性，作者在 Lean 中验证了主要定理陈述及所接受的公理。本文讨论了针对 AI 生成形式化所做的修正与简化，并记录了形式化过程中发现的论文中的差异。Lean 代码可在该 https URL 获取。
英文摘要
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.
发表机构
- The Chinese University of Hong Kong, Shenzhen（香港中文大学（深圳））
机构由 AI 辅助整理，请以论文原文为准。
