Formalizing Free Groups in Isabelle/HOL: The Nielsen-Schreier Theorem and the Conjugacy Problem. - Aabid Seeyal Abdul Kharim; T. V. H. Prathamesh; Shweta Rajiv; Rishi Vyas (CICM, 2023)