Abstract
We present a formalization of Lyndon words and basic relevant results in Isabelle/HOL. We give a short review of Isabelle/HOL and focus on challenges that arise in this formalization.
The presented formalization is based on an ongoing larger project of formalization of combinatorics on words