Paper · 3 pages · 1 October 2026
The sphere-covering bound in Lean
Abstract
We formalize the classical sphere-covering lower bound on the covering number Kq(n,R) in Lean 4, against Mathlib v4.34.1. The library proves that every code over Z/qZ of length n which covers the space at Hamming radius R has at least ⌈qn/V⌉ words, where V is the size of a Hamming ball, and it checks eight numerical instances, including K7(9,4) ≥ 221. The same archive determines several small covering numbers exactly, among them K2(7,1) = 16 by the binary Hamming code of length 7, and it exhibits a 12-word covering of (F2)6 at radius 1. It does not prove matching upper bounds for the eight instances, does not decide whether those lower bounds improve the literature, and leaves K2(6,1) ≥ 11 conditional on a search the kernel did not finish.
The eight checked lower bounds
| q | n | R | V | ceiling |
|---|---|---|---|---|
| 5 | 7 | 2 | 365 | 215 |
| 4 | 10 | 4 | 20686 | 51 |
| 5 | 9 | 3 | 5989 | 327 |
| 5 | 10 | 4 | 62201 | 158 |
| 5 | 9 | 5 | 167269 | 12 |
| 5 | 9 | 4 | 38245 | 52 |
| 7 | 8 | 3 | 13153 | 439 |
| 7 | 9 | 4 | 182791 | 221 |
Each number is a lower bound on every covering code. None of them is a construction. K7(9,4) ≤ 1351 is not a theorem in this paper.