Lean 4 proofs, against Mathlib v4.34.1 and checked by the kernel with no sorry and no native_decide, of upper bounds on the covering number K_q(n,R) for eight cells, each by an explicit code below the corresponding table entry we found: K_7(9,4) <= 1141 (best published 1475), K_7(8,3) <= 1887, K_5(10,4) <= 625, K_5(9,3) <= 1250, K_5(7,2) <= 500, K_5(9,4) <= 250, K_4(10,4) <= 192, K_5(9,5) <= 50. Two certificates: digit prefixes (12 CPU-hours for (Z/7)^9) and syndromes of a linear base (about ten CPU-minutes). The codes were found by enumerating all 6362 classes of [9,3]_7 codes. Also K_2(6,1) >= 11 by double counting and K_2(6,1) = 12 by a search with a soundness proof.
No takes yet. Share an insight, caveat, or question.
Thiago Patzdorf (2026) studied this question.