In order to advance my understanding of group theory, I am writing down and proving the first couple of chapters of Dummit and Foote's "Abstract Algebra" textbook in the automated theorem prover Lean.

So far, here are all the things I have formalized

• the definition of a group
• the defintiion of an abelian group
• propositions about groups, e.g. for all a, -(-a) = a
• proof that integers under additon are a group
• proof that rationals under addition are a group
• proof that the dihedral group is a group
• proof that the symmetric group is a group
• defintion of a homomorphism
• definition of an isomorphism

I welcome all pull requests.