Formalizing Free Groups in Isabelle/HOL: The Nielsen-Schreier Theorem and the Conjugacy Problem

Free groups are central to group theory, and are ubiquitous across many branches of mathematics, including algebra, topology and geometry. An important result in the theory of free groups is the Nielsen-Schreier Theorem, which states that any subgroup of a free group is free. In this paper, we present a formalisation, in Isabelle/HOL, of a combinatorial proof of the Nielsen-Schreier theorem. In particular, our formalisation applies to arbitrary subgroups of free groups, without any restriction on the index of the subgroup or the cardinality of its generating sets. We also present a formalisation of an algorithm which determines whether two group words represent conjugate elements in a free group. To the best of our knowledge, our work is the first formalisation of a combinatorial proof of the Nielsen-Schreier theorem in any proof assistant; the first formalisation of a proof of the Nielsen-Schreier theorem in Isabelle/HOL; and the first formalisation of the decision process for the conjugacy problem for free groups in any proof assistant.