Formalization of Combinatorics on Words in Isabelle/HOL
We introduce our project devoted to formalization of Combinatorics on Words in Isabelle/HOL. We start from basic facts suitable for educational purposes with the prospect of more complicated research objectives (including long standing open questions concerning equations on words).
We believe that combinatorics of words is an area where computer assisted formalization may be very helpful, due to the fact that proofs of even fairly simple results tend to be tedious and repetitive.
|Formalization of Combinatorics on Words in Isabelle/HOL (LightningCPP2021.pdf)||214KiB|