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.

翻译：我们在 Lean 4 中严格证明了八进制覆盖码的精确值 $K_8(4,2)=23$。上界由显式给出的 23 个码字、半径为 2 的代码（定义在 $(Fin\:8)^4$ 上）确定，该代码已对所有 $8^4$ 个环境词进行全覆盖检验。下界则排除了包含至多 22 个码字的覆盖方案。首先通过纤维计数与缺失对论证排除了包含至多 21 个码字的覆盖方案。在剩余的 22 码字情形中，证明将假设的覆盖方案简化为六个源自坐标对投影的缺失对图。纤维计数论证约束了这些图的结构，而两个由 Lean 校验的线性分辨率反证（LRAT）对存储的合取范式（CNF）实例进行反驳，强制要求形成共同的 3+3+2 分块结构。该结构与 22 码字覆盖方案矛盾：两个三符号分量已强制要求 18 个码字，而剩余的双符号分量需要宽度为 4 且最多 4 行的二进制强度二数组，这是不可能的。最终结果打包为携带证明的 Lean 工件：显式上界、结构化下界、CNF 实例及 LRAT 反证均在 Lean 内部完成校验，证明重放过程中无需外部 SAT 求解器参与。