Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4
2026-06-08 • Information Theory
Information Theory
AI summaryⓘ
The authors created a formalized math framework in the Lean 4 proof assistant to study covering codes, which are small sets of words that together cover all possible words within a certain distance. They proved key formulas and bounds about these codes, including exact small cases, and connected their results to previous work by van Laarhoven and colleagues. Their main goal was to build a reliable and checkable system for verifying covering code bounds, not to find new results but to ensure correctness through machine-checked proofs. This system stores all data with proof traces that can be replayed to confirm each bound rigorously.
covering codesHamming spaceq-ary codesHamming ballcovering radiusLean 4formal proofsphere-covering boundproof assistantmachine-checked proofs
Authors
Andreas Florath
Abstract
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.