Warning: not (yet) a game!
What this repo has become is a development of group theory from scratch in Lean (i.e. using our own definition of group rather than the one in mathlib). We get as far as a proof of Sylow's first theorem!
Ultimately we should be able to turn this into a game where people can develop group theory themselves in Lean.
This repo was developed by Kevin Buzzard, Kexing (Jason) Ying, and Giulia Carfora. Giulia was supported by a Mary Lister McCammon Fellowship.