Group Action Exercises

Important

This is WIP right now. Feedback welcome in issues.

What is this repo?

A collection of exercises intended to teach a student who is proficient in group theory how to use Lean's inbuilt theory of group actions.

Thanks to Ines Wright for asking good questions.

How to play?

The proper way

1. Install the leanprover-community python tool leanproject, giving you the ability to download Lean projects onto your computer. Instructions on how to do this are on the community website.

2. leanproject get ImperialCollegeLondon/group-action-exercises in the command line (yes I know, we're working on it)

3. Open the new folder group-action-exercises which has just appeared on your computer.

Have a play with level_1_groups.lean in the /src directory, and the other files in that directory.

the quick way

You think you're saving time, but Lean runs much slower, so if you play for long enough you'll have lost outright.

direct link to level 1 in the Lean web editor

direct link to level 2 in the Lean web editor