A Lean-Certified Proof of $K_8(4, 2) = 23$
2026-06-15 • Information Theory
Information Theory
AI summaryⓘ
The authors determined the exact minimum size of a special kind of code in an eight-symbol, four-length setting, proving it is 23. They did this by providing an example with 23 codewords and proving no smaller set can cover all required words. Their proof uses a detailed counting method and graph arguments, along with computer-checked logic proofs inside the Lean 4 system, without relying on external SAT solvers. This is packaged as a rigorously checked digital proof artifact.
covering codeoctonary coderadius-two codeLean 4fiber-countingmissing-pair graphsLRAT refutationCNF instancesSAT solverproof-carrying artifact
Authors
Andreas Florath
Abstract
We prove the exact octonary covering-code value $K_8(4, 2) = 23$ in Lean 4. The upper bound is given by an explicit 23-word radius-two code in $(Fin\:8)^4$ , checked over all $8^4$ ambient words. The lower bound excludes covers with at most 22 words. A fiber-counting and missing-pair argument first rules out covers with at most 21 words. In the remaining 22-word case, the proof reduces a hypothetical cover to six missing-pair graphs coming from the coordinate-pair projections. Fiber-counting arguments constrain these graphs, and two Lean-checked Linear RAT (LRAT) refutations of stored conjunctive-normal-form (CNF) instances force a common 3 + 3 + 2 block structure. This structure is incompatible with a 22-word cover: the two three-symbol components already force 18 codewords, while the remaining two-symbol component would require a binary strength-two array of length four with at most four rows, which is impossible. The result is packaged as a proof-carrying Lean artifact: the explicit upper bound, structural lower bound, CNF instances, and LRAT refutations are checked inside Lean, with no external SAT solver used during proof replay.