Covering codes checked by the Lean kernel: K_7(9,4) <= 1351 and K_2(6,1) = 12
Open access0 citations
Abstract
Lean 4 proofs, against Mathlib v4.34.1 and checked by the kernel with no sorry and no native_decide, of three results on the covering number K_q(n,R): an explicit 1351-word code shows K_7(9,4) <= 1351, below the best published upper bound we found (1475, Marosi 2026); K_2(6,1) >= 11 by a double-counting argument without search; and K_2(6,1) = 12 by a pruned search with a soundness proof. The library also formalizes the sphere-covering bound. Seven further codes improving the tables we consulted are verified by computer only.
// Source
View paper (DOI)Open access versionOpenAlexZenodo (CERN European Organization for Nuclear Research)Published 2026-10-02
Authors: Thiago Patzdorf
Institutions: Universidade de Caxias do Sul