Summary
2020
Session Number:E03
Session:
Number:E03-1
Formalization of VT Codes and Their Single-Deletion Correcting Property in Lean
Yuki Kondo, Manabu Hagiwara, Midori Kudo,
pp.597-601
Publication Date:2020/10/18
Online ISSN:2188-5079
PDF download
Summary:
This manuscript reports on our project on formalization for deletion codes in Lean theorem prover: the definition of Varshamov-Tenengolts (VT) codes and their single-deletion error-correcting property are formalized. It also reports progress on our attempt to resolve an open problem of VT codes in Lean.