advanced MiL exercises

Stream: Lean for teaching

[Rob Lewis]

Is there a list/repository anywhere of "advanced" exercises for people working through MiL? I have a student working through it very quickly, and would love to suggest some problems that are more open-ended than what's in the textbook but not project-level difficulty.

[Patrick Massot]

Exercises in the last chapters are a lot more challenging than in the early chapters. The last file of the tutorial project is also more challenging.

[Jeremy Avigad]

I'd suggest picking any theorem they have learned in a class or proved as a homework exercise and trying it. It doesn't matter whether the theorem is in Mathlib; for example, they may formalize a direct proof of the intermediate value theorem.