Given a finite
presentation of a group $G$, proving properties of $G$
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.