3 papers
cs.IT2026
A Lean-Certified Proof of
Andreas Florath
We prove the exact octonary covering-code value in Lean 4. The upper bound is given by an explicit 23-word radius-two code in , checked over all …
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…
cs.DL2026
Aletheia-Probe: A Tool for Automated Journal Assessment
Andreas Florath
Assessing journal legitimacy during literature reviews, publication venue selection, and citation verification requires consulting information scattered across multiple incompatibl…