🔢 mathematics

Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4

This paper presents a formalization of the elementary theory of q-ary covering codes in Lean 4, establishing a reusable, auditable foundation with proof-carrying certificates for verifying upper and lower bounds on covering numbers.

Original authors: Andreas Florath

Published 2026-06-09

📖 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 cover a giant, multi-dimensional chessboard with a limited number of "safety nets."

In the world of mathematics, this is the problem of Covering Codes. You have a grid of possible positions (like a chessboard, but it could be 3D, 4D, or even higher dimensions). You want to place a small number of "centers" on this grid. The rule is that every single square on the board must be within a certain distance (let's say, one step) of at least one of your centers.

The big question is: What is the absolute minimum number of centers you need to cover the entire board?

This paper, written by Andreas Florath, doesn't try to find a new record for the smallest number of centers. Instead, it builds a digital, unbreakable vault to prove that the numbers we already know are correct.

Here is a breakdown of the paper's ideas using simple analogies:

1. The "Proof-Carrying Certificate" (The Golden Ticket)

Usually, when a mathematician says, "I found a code with 73 centers that covers the board," they show you a list of numbers. You have to trust them, or spend hours checking the math yourself.

This paper introduces a "Proof-Carrying Certificate." Think of this not just as a list of numbers, but as a Golden Ticket that comes with a built-in, self-checking magic trick.

The Ticket: It says, "Here is a set of 73 centers."
The Magic Trick: The ticket contains a tiny, automated robot (written in a language called Lean 4) that instantly checks every single square on the board to confirm: "Yes, this square is covered. Yes, that square is covered. Yes, all of them are."
The Result: You don't have to trust the author. You just run the robot. If the robot says "Pass," the proof is 100% mathematically guaranteed.

2. The "Two-Part Puzzle"

To prove you have the perfect (exact) number of centers, you need to solve two different puzzles at once:

The Upper Bound (The Construction): "I can cover the board with 73 centers." (You show the list).
The Lower Bound (The Impossible Task): "It is impossible to cover the board with 72 centers." (You prove that no matter how you try, you will always leave a hole).

The paper builds a system where these two puzzles are separate pieces. You can have a certificate for the "73" and a separate certificate for the "impossible with 72." When they meet, they snap together to form a perfect, exact answer.

3. The "Lego" of Math

The author built a massive library of Lego bricks (formal rules).

Some bricks are simple: "If you cover a small board, you can cover a bigger board by adding a few more pieces."
Some bricks are complex: "If you combine two different types of boards, here is exactly how the covering rules change."

The beauty of this paper is that these bricks are interchangeable. If someone else finds a new way to cover a board, they can just snap their new brick into this existing Lego structure, and the whole system automatically verifies it.

4. The "Database of Truth"

The paper includes a Proof-Carrying Database. Imagine a library book where, instead of just printing the answer "The answer is 7," the book includes a video recording of the proof.

If you look up a number in this database, it doesn't just give you a number. It gives you the trace (the step-by-step video) of how that number was proven.
You can replay this video in the Lean 4 system, and it will re-run the proof from scratch to make sure it still holds up.

5. The "Football Pool" Example

The paper uses a real-world analogy to explain the problem: The Football Pool.
Imagine you are betting on 8 soccer matches. Each match has 3 possible outcomes (Win, Draw, Loss). You want to buy a set of betting tickets.

The Goal: No matter what the actual results are, you want to guarantee that at least one of your tickets is "close" (maybe only 1 prediction wrong).
The Math: How many tickets do you need to buy to guarantee this?
The Paper's Role: The paper takes a famous, published solution for this problem (where someone found a set of 486 tickets) and turned it into a machine-checkable certificate. It proves, beyond any doubt, that 486 tickets work.

What This Paper Actually Claims (and What It Doesn't)

It DOES claim: It has built a solid, reusable foundation (a "formal foundation") where covering code proofs can be stored, checked, and combined automatically. It has verified several specific, known numbers (like the 486 tickets for the 8-match problem) using this new system.
It DOES NOT claim: It does not claim to have found a new record for the smallest number of tickets needed. It does not claim to solve the problem for every possible scenario. It is a tool-building paper, not a record-breaking paper.

The Big Picture

Think of this paper as building a high-security vault for mathematical truths. Before, if you wanted to check a complex covering code, you had to trust a human or a computer program that might have a bug. Now, thanks to this paper, you have a system where the proof itself is a piece of software that you can run to verify the truth instantly. It turns "I think this is right" into "The computer has proven this is right."

Technical Summary: Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4

Problem Statement
Covering codes in finite Hamming spaces seek the smallest set of words (codewords) such that the union of their Hamming balls of radius $r$ covers the entire space $A^n$ . The central quantity is the $q$ -ary covering number $K_q(n,r)$ , defined as the minimum size of such a code. While the definition is elementary, determining exact values or tight bounds for $K_q(n,r)$ typically relies on a mixture of explicit constructions, counting arguments, recursive relations, and computer searches. A significant challenge in the field is that exact statements $K_q(n,r) = k$ require two independent components: an explicit construction proving an upper bound ( $K_q(n,r) \le k$ ) and a proof that no smaller code exists (a lower bound $K_q(n,r) \ge k$ ). These components often originate from disparate sources, making the verification of exact values difficult to audit.

Methodology
The paper presents a formalization of elementary covering code theory in the Lean 4 theorem prover. The methodology is characterized by three core design choices:

Representation of Words: Words are modeled as dependent functions from a coordinate type to an alphabet type. The general $q$ -ary Hamming space of length $n$ is represented as Fin n → Fin q. This functional representation preserves a general interface for abstract coordinate types while simplifying the $q$ -ary specialization.
Certificate-Style Predicates: Instead of defining $K_q(n,r)$ $K_{q} (n, r)$ as a noncomputable minimization function, the formalization uses logical predicates to represent assertions about covering numbers.
- KUpper r k: Asserts the existence of a finite covering code of size at most $k$ (upper bound).
- KLower r k: Asserts that every finite covering code has size at least $k$ (lower bound).
- KSpec r k: Combines both to assert exactness ( $K_q(n,r) = k$ ).
  This modular approach allows upper and lower bounds from different sources to be assembled independently.
Proof-Carrying Database: The paper implements a database where stored bounds are not merely numerical values but "proof-carrying" objects. Each entry includes a derivation trace. Replaying this trace in Lean reconstructs a formal proof of the corresponding QaryKUpper or QaryKLower predicate. The system distinguishes between handwritten mathematical theorems (kernel-checked) and generated data (untrusted producers whose output is validated via trace replay).

Key Contributions
The paper establishes a reusable, auditable foundation for machine-checked covering-code certificates. Its specific contributions include:

Formal Infrastructure: A complete Lean 4 framework for finite Hamming spaces, Hamming distance, closed balls, and covering predicates, handling edge cases (e.g., $q=0$ , $n=0$ , $r \ge n$ ) rigorously within the definitions rather than as informal conventions.
Analytical Results: Formal proofs of the $q$ -ary Hamming-ball volume formula and the classical sphere-covering lower bound. The sphere-covering bound is encapsulated as a computable function sphereLower that generates certified lower-bound certificates.
Structural Theorems: Formalization of elementary exact cases (e.g., $K_q(n,0) = q^n$ , $K_q(n, n-1) = q$ ) and structural constructions, including a product covering theorem and various neighbor relations (puncturing, lengthening, alphabet projection, and concatenation) that transport bounds between parameter triples.
Case Study (Van Laarhoven et al.): An end-to-end workflow demonstrating the formalization of published explicit codes. The authors transcribed covering codes from a 1989 paper (Van Laarhoven et al.) into Lean, encoding them as packed arrays to avoid elaboration limits. The system verified the covering property and cardinality, producing machine-checked upper-bound certificates for $K_3(6,1) \le 73$ , $K_3(7,1) \le 186$ , and $K_3(8,1) \le 486$ .
Database Implementation: A proof-carrying database containing 52,822 entries for parameters $0 \le q \le 21$ , $0 \le n \le 48$ , and $0 \le r \le 48$ . This database includes exact certificates for small cases (e.g., $K_2(5,1)=7$ , $K_3(3,1)=5$ ) and intervals derived from trace replay.

Results
The formalization successfully verifies:

The $q$ -ary ball volume formula and the sphere-covering lower bound.
Elementary exact values such as $K_2(5,1)=7$ , $K_2(6,2)=4$ , $K_3(3,1)=5$ , and $K_4(3,1)=8$ .
Upper bounds for the ternary football-pool problem derived from explicit codes, specifically $K_3(6,1) \le 73$ , $K_3(7,1) \le 186$ , and $K_3(8,1) \le 486$ .
A uniform two-block cyclic construction proving $K_q(3,1) \le \lceil q^2/2 \rceil$ .

The database closure process successfully propagated these primitive sources through certified relation rules to generate a consistent table of bounds. The system supports two proof modes: a "kernel mode" using standard decide for stronger replay guarantees, and a "native mode" using Lean's compiled evaluator for faster development, with clear trust boundaries defined for each.

Significance and Claims
The paper explicitly states that its primary contribution is not the discovery of new record-breaking bounds or the reproduction of existing literature tables. Instead, its significance lies in providing a formal interface and auditable foundation for covering-code certificates.

The work bridges the gap between classical covering-code literature and future computational certificates. By separating upper-bound witnesses, lower-bound arguments, and exactness predicates, the formalization allows results from explicit constructions, combinatorial counting, and (potentially) future SAT or integer-programming solvers to be checked and composed within a single trusted framework. The "proof-carrying" nature of the database ensures that every reported bound can be traced back to a machine-checked proof, addressing the reproducibility and verification challenges inherent in the field. The paper positions itself as a foundational step toward a future where computational search results can be seamlessly integrated into formal mathematical libraries.