Thiago Patzdorf

Covering codes checked by the Lean kernel: K_7(9,4) <= 1134, ten more upper bounds, K_2(6,1) = 12, and K_7(4,2) = 19

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 eleven cells, each by an explicit code below the corresponding table entry we found: K_7(9,4) <= 1134 (best published 1475, Mar...

Covering codes checked by the Lean kernel: K_7(9,4) <= 1351 and K_2(6,1) = 12

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) >=...

Covering codes checked by the Lean kernel: K_7(9,4) <= 1137, seven more upper bounds, and K_2(6,1) = 12

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) <= 1137 (best published 1475, Maro...