Joachim Breitner's Homepage

Since a few months, I have been playing around with Isabelle, a theorem prover system. I find it very intriguing to have proofs of mathematical statements checked by something as pendantic and comprehensive as a machine. Mathematicians always claim that their statements are true in all eternity, but the proofs are just checked by error-prone human beings. Especially with complex, large proofs that are only read by a handful of people, I doubt that these are always fully correct. Note that this does not imply that I doubt that the results are correct. They probably are. But a bit of doubt remains. A computer-checked proof, in contrast, can not accidentially omit corner cases, leave out seemingly “trivial” assumtions of used theorems or be misled by slightly differing definition from different sources.

I was hoping to check at least parts of my diploma thesis using Isabelle, but it turns out that the standard algebra library shipped with Isabelle is not complete enough. Even free groups were missing. This was motivation enough to try to formalize them and prove the universal property and some isomorphisms (The free group over the empty set is the unit group, the free group over one generator is the additive group of integers and free groups over sets of same cardinality are isomophic). I submitted the resulting theory to the Archive of Formal Proofs and it was accepted. You can view the complete document or the document without proofs.

I did not formalize the fact that isomorphic free groups have bases of same cardinality. As far as I know there is no simple argument that works directly with free groups. The proofs I have seen pass to the abelianization of the free group, i.e. the free module over ℤ and apply the well known proof from the analogous statement about vector spaces. But if someone knows an elementary proof of this fact, I’d like to hear about it.