Formalization of VT Codes and Their Single-Deletion Correcting Property in Lean. - Yuki Kondo; Manabu Hagiwara; Midori Kudo (ISITA, 2020)