Group theoretic proofs by coset enumeration

Given a finite presentation of a group, proving properties of the group can be difficult. Indeed, many questions about finitely presented groups
are unsolvable in general.  Algorithms exist for answering some questions while for other questions algorithms exist for verifying the truth of
positive answers.  An important tool in this regard is the Todd-Coxeter coset enumeration procedure.  It is possible to extract formal proofs
from the internal working of coset enumerations.  We give examples of how this works, and show how the proofs produced can be mechanically verified
and how they can be converted to alternative forms.  We discuss these automatically produced proofs in terms of their size and the insights
they offer. We compare them to hand proofs and to the simplest possible proofs.  We point out that this technique has been used to help solve
a longstanding conjecture about an infinite class of finitely presented groups.