🔢 mathematics

A Lean-Certified Proof of $K_8(4, 2) = 23$

This paper presents a fully formalized proof in Lean 4 that the octonary covering code value $K_8(4, 2)$ equals 23, establishing the upper bound via an explicit 23-word code and the lower bound by combining fiber-counting arguments with LRAT-refuted CNF instances to demonstrate that no 22-word cover can exist.

Original authors: Andreas Florath

Published 2026-06-16

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Andreas Florath

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to pack a set of special "safety nets" into a giant, four-dimensional room filled with millions of points. The goal is to ensure that every single point in the room is within a short distance (let's say, two steps) of at least one safety net.

The question mathematicians have been asking is: What is the absolute minimum number of safety nets you need to cover the entire room?

For a specific type of room (where each dimension has 8 possible values), the answer has been narrowed down to a tiny range: it's either 22 nets or 23 nets. This paper, written by Andreas Florath, proves definitively that 23 is the magic number. You cannot do it with 22.

Here is how the proof works, broken down into simple analogies:

1. The Two-Part Proof

To prove the answer is exactly 23, the author had to do two things, like proving a door is locked from both sides:

The Upper Bound (Showing 23 works): The author simply found a specific list of 23 safety nets and checked them against every single point in the room. It's like saying, "Here is a map of 23 fire stations; I've walked every street and confirmed that no house is more than two blocks away from a station." This part is easy to verify because the author just showed the list.
The Lower Bound (Showing 22 fails): This is the hard part. The author had to prove that it is impossible to cover the room with only 22 nets. You can't just check every possible arrangement of 22 nets because there are too many (more than the atoms in the universe). Instead, the author used a clever logic trick to show that any attempt to use 22 nets would inevitably leave a hole.

2. The "Missing Pair" Detective Work

To prove 22 nets aren't enough, the author didn't look at the nets directly. Instead, they looked at what was missing.

Imagine the room is a giant grid. If you pick any two coordinates (like "floor" and "wall"), you can look at all the pairs of values that appear in the nets.

The Logic: If a specific pair of values (e.g., "Floor 3, Wall 5") never appears together in any of your 22 nets, that's a "missing pair."
The Graph: The author drew a map (a graph) for every pair of coordinates, marking the "missing" combinations.
The Contradiction: The proof shows that if you only have 22 nets, the rules of geometry force these "missing pair" maps to form a specific, forbidden shape—a "clique" (a tight knot of missing connections). But if that shape exists, it means there is a point in the room that is too far away from any of your nets. Therefore, 22 nets cannot cover the room.

3. The "Block" Puzzle

When the author analyzed the case where someone tries to use exactly 22 nets, they found that the nets would have to arrange themselves in a very rigid, block-like structure (specifically a 3 + 3 + 2 pattern).

Think of it like trying to build a wall with 22 bricks. The math shows that to avoid holes, the bricks would have to be stacked in three specific groups. However, when you try to build the final section of the wall using the remaining bricks, the geometry breaks down. It's like trying to fit a square peg into a round hole; the structure required to cover the room simply cannot exist with only 22 pieces.

4. The "Lean" Computer Check

This is where the paper gets high-tech. Because the "missing pair" logic involves checking thousands of tiny possibilities (like a Sudoku puzzle with millions of cells), the author used a computer program called Lean.

The SAT Solver: The author used a powerful computer program (a SAT solver) to check the massive list of possibilities and say, "This specific arrangement is impossible."
The Certificate: Usually, we have to trust the computer. But here, the computer didn't just say "Impossible." It produced a certificate (a step-by-step receipt of its logic).
The Verification: The Lean program then read that receipt and verified every single step of the computer's logic itself. This means the proof is machine-checked. We don't have to trust the computer's brain; we only have to trust the Lean program's ability to read the receipt, which is much smaller and easier to verify.

Summary

The paper proves that for this specific 4-dimensional room with 8 options per dimension:

23 nets are enough (here is the list).
22 nets are not enough (here is a logical proof that any attempt to use 22 nets creates an unavoidable gap).

The result is a "Lean-Certified" proof, meaning the entire argument—from the big logic down to the tiny computer checks—has been verified by a formal mathematical software system, leaving no room for human error or doubt. The answer is exactly 23.

Technical Summary: A Lean-Certified Proof of $K_8(4,2) = 23$

Problem Statement
The paper addresses the determination of the exact covering number $K_q(n,r)$ , defined as the minimum size of a radius- $r$ covering code in the $q$ -ary Hamming space of length $n$ . Specifically, it resolves the value for the octonary case with length 4 and radius 2: $K_8(4,2)$ . Prior to this work, existing bounds (specifically Kéri's tables) placed this value in the interval $[22, 23]$ . The lower bound was derived from the Rodemich rook-domain bound, while the upper bound was supported by large-alphabet bounds. The objective was to close this interval by proving the lower bound $K_8(4,2) \ge 23$ .

Methodology
The proof is formalized in the Lean 4 theorem prover using the mathlib library. It employs a "proof-carrying" approach where the result is established via two independent certificates: an explicit upper bound and a structural lower bound.

Upper Bound ( $K_8(4,2) \le 23$ ):
The authors provide an explicit code consisting of 23 codewords in $(\text{Fin } 8)^4$ . The formal proof verifies two conditions: the cardinality of the set is at most 23, and every word in the ambient space (4096 words) is within Hamming distance 2 of at least one codeword. This is an exhaustive finite check.
Lower Bound ( $K_8(4,2) \ge 23$ ):
The core of the paper is a structural non-existence argument for any hypothetical cover $C^*$ with $|C^*| \le 22$ . The proof proceeds through a sequence of reductions:
- Fiber Counting: For a hypothetical cover, the authors define "fibers" $C^*_{i,a}$ (codewords with symbol $a$ at coordinate $i$ ). They prove that every fiber must contain at least two codewords. This establishes a baseline of 16 codewords ( $8 \text{ symbols} \times 2$ ) per coordinate, leaving a "budget" of at most 6 excess codewords for the case $|C^*|=22$ (or 5 for $|C^*| \le 21$ ).
- Missing-Pair Graphs: The proof shifts to an "inverse" viewpoint, analyzing which pairs of symbols are missing from the projections of the code onto coordinate pairs. These missing pairs form graphs $E_{ij}$ .
- Case $|C^*| \le 21$ : Using the small excess budget, the authors demonstrate via combinatorial counting that the missing-pair graphs must contain a "simultaneous four-partite clique" (a set of four symbols $a,b,c,d$ such that all six coordinate pairs are missing). Lemma 7 proves that such a clique cannot exist in a valid radius-2 cover, thereby ruling out covers of size 21 or fewer.
- Case $|C^*| = 22$ : For the remaining case, the proof reduces the problem to a finite classification of the "profile" of the missing-pair graphs. The authors show that any valid profile must exhibit a specific "common $3+3+2$ block structure."
- SAT/LRAT Integration: The classification of these profiles is too large for manual enumeration. The authors encode the constraints (row/column degree bounds and the no-clique condition) into Conjunctive Normal Form (CNF) instances. They use an untrusted SAT solver to generate Linear RAT (LRAT) refutations (proofs of unsatisfiability).
- Formal Verification: Lean parses these LRAT certificates and mechanically replays the refutations to prove that no valid profile exists for a 22-word cover.
- Final Contradiction: Even if a common block structure were assumed, the authors derive a contradiction in the "2-symbol component" of the structure. This component would require a binary strength-2 array of length 4 with at most 4 rows, which is mathematically impossible.

Key Contributions

Exact Value: The paper establishes the exact value $K_8(4,2) = 23$ , closing the previously known interval $[22, 23]$ .
Formalized Lower Bound: It provides a fully formalized proof in Lean 4 that excludes all 22-word covers. This is achieved not by volume arguments but by structural obstructions derived from fiber counts and missing-pair graphs.
Proof-Carrying Artifact: The result is packaged as a Lean artifact containing the explicit code, the structural lemmas, the CNF instances, and the LRAT refutations. Crucially, the SAT solver is not part of the trusted computing base; Lean verifies the LRAT certificates internally.
Pattern for Computational Lower Bounds: The paper introduces a reusable pattern for attaching solver-produced evidence to covering-code lower bounds. It separates the "discovery" (untrusted solver) from the "verification" (trusted Lean kernel), allowing large finite classification problems to be solved computationally while maintaining formal correctness.

Results
The primary result is the theorem $K_8(4,2) = 23$ .

Upper Bound: Proven by an explicit 23-word code.
Lower Bound: Proven by showing that a cover of size 22 leads to a contradiction via a forced "common $3+3+2$ block system" which implies the existence of an impossible binary array.
Performance: The formal verification involves significant computational resources. The kernel-mode replay of the main proof file required approximately 143 GiB of RAM, while native mode reduced this to roughly 5.5 GiB. The LRAT checking phase took approximately 17 minutes in kernel mode.

Significance and Claims
The paper claims significance primarily in the realm of formalized mathematics and the methodology of combining combinatorial reasoning with computational certificates.

Methodological Shift: It demonstrates that structural combinatorics can be combined with "proof-carrying" computational evidence. The SAT solver is used to discover finite obstructions, but the mathematical bridge and the verification of the solver's output are handled entirely within the theorem prover.
Trust Boundary: The work clarifies the trust boundary in formal proofs involving SAT solvers. The solver is untrusted; the Lean kernel checks the LRAT certificates and the logical deduction that connects these certificates to the covering code statement.
Scalability: The result serves as a test case for handling covering-code problems that are too large for manual proof but small enough to be reduced to finite classification problems solvable by SAT solvers.
No New Applications: The paper does not claim new applications for the value $K_8(4,2)=23$ itself, nor does it propose new experimental protocols. Its contribution is strictly the resolution of a specific open problem in coding theory tables and the demonstration of a formal verification workflow for such problems.