Ines Wright: 'Formalising Nilpotent Groups in Lean'

Ines formalised one of Sylow's Theorems and also some of the basic theory of nilpotent groups in her 2021 summer project. Here she talks about her work on nilpotent groups. Some of her worked has been made into succesful mathlib PRs.