Master’s practical course, Master’s thesis, or IDP
The purpose of this project is to add various missing bits of group theory to HOL-Algebra, with a particular focus on finite groups. Topics of interest include:
- Decomposition of a group into an interior direct product
- Indexed direct products
- The fundamental theorem of finite(ly generated) abelian groups
- Finite simple groups
Experience with Isabelle/HOL is required. Knowledge of basic group theory is recommended. Experience with locales or even HOL-Algebra itself would be helpful, but is not required.