Andreas Florath

collaborators

Showing cs.ITShow all

2 papers · 1 filter

cs.IT2026

A Lean-Certified Proof of $K_{8} (4, 2) = 23$

Andreas Florath

We prove the exact octonary covering-code value $K_{8} (4, 2) = 23$ in Lean 4. The upper bound is given by an explicit 23-word radius-two code in $(F in 8)^{4}$ , checked over all $8^{4}$ …

cs.IT2026

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

Andreas Florath

Covering codes in finite Hamming spaces ask for small sets of words whose Hamming balls cover the whole space. This paper presents a Lean 4 formalization of the elementary theory o…

A Lean-Certified Proof of K8​(4,2)=23

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

A Lean-Certified Proof of $K_{8} (4, 2) = 23$