Andreas Florath

activity

20232026

most citedEnhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code

1 citations · 2 across the 5 of their papers we have counts for

collaborators

Showing 2026 · cs.ITShow all

2 papers · 2 filters

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$