Covering codes in finite Hamming spaces ask for small sets of words whose Hamming balls cover the whole space. This paper presents a Lean 4 formalization of the elementary theory of q-ary covering codes, centered on certificate predicates for upper bounds, lower bounds, and exact covering numbers $K_q(n,r)$. The formalization proves the q-ary Hamming-ball volume formula, the sphere-covering lower bound, elementary exact cases, product and relation rules, and selected small exact certificates. It also demonstrates an end-to-end workflow for checking explicit upper bounds transcribed from van Laarhoven et al. (1989). The accompanying database is proof-carrying: stored bounds have traces that replay to Lean proofs of the corresponding upper- or lower-bound predicates. The contribution is not new record bounds or a reproduction of known tables, but a reusable, auditable foundation for machine-checked covering-code certificates.

翻译：有限汉明空间中的覆盖码问题要求寻找一个小的词集合，使得这些词的汉明球覆盖整个空间。本文给出了q元覆盖码基础理论的Lean 4形式化，重点围绕上界、下界及精确覆盖数$K_q(n,r)$的证书谓词展开。该形式化证明了q元汉明球体积公式、球覆盖下界、基本精确情形、乘积与关系规则，以及选定的精确小规模证书。此外，本文还展示了从van Laarhoven等人(1989)转录的显式上界进行端到端检验的工作流程。所附数据库具有证明携带特性：存储的界值带有可回溯至Lean证明的踪迹，这些证明对应相应的上界或下界谓词。本工作的贡献不在于创造新的界值记录或复现已知表格，而是为机器可检验的覆盖码证书提供了一个可复用、可审计的基础框架。