search

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
https://adam.math.hhu.de
Apache License 2.0
16 stars 9 forks source link

MatrixTrace, Level 9: everyone gets stuck #43

Closed TentativeConvert closed 2 months ago

TentativeConvert commented 3 months ago

This levels appears to be very difficult. I think part of the problem is that students start the planet one week and then try to finish it the next week. By that time, they’ve forgotten all lemmas that they already proved, and get stuck at places like:

https://github.com/hhu-adam/Robo/blob/20750845be33e8e6f91b3811d264202ee0cc7b91/Game/Levels/MatrixTrace/L09_EvalOnEBasis.lean#L83

And I also don’t know how to proceed because I don’t know all lemmas that have already been proved off the top of my head.

TentativeConvert commented 2 months ago

I have added more explanations to levels 8 and 9, and partially rewritten level 9: 5c175781ba6a91ad0c3e2cc074b150ce43d0928d, bed81540be524ee91e5b34950543faaa4609ba7d