If you download this Lean project onto your own computer using leanproject by typing leanproject get ImperialCollegeLondon/Example-Lean-Projects you will just be able to edit it and experiment with it. It's lots of Lean projects, some big, some small, all in their own directories, but often with sorries. Try filling in the sorries!

There are other projects which are readable and have half-written code and opportunities to fill in proofs of theorems. Here are some examples:

• The complex number game.

leanproject get ImperialCollegeLondon/complex-number-game

• Some commutative algebra experiments

leanproject get ImperialCollegeLondon/M4P33

• Building group theory from scratch

leanproject get ImperialCollegeLondon/group-theory-game

• Galois theory experiments

leanproject get ImperialCollegeLondon/P11-Galois-Theory

• Basics of Clausen/Scholze theory of condensed sets

leanproject get ImperialCollegeLondon/condensed-sets