Formalization of VT Codes and Their Single-Deletion Correcting Property in Lean

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.