> for education Is there any standard curriculum course for... this? (Actually, I don't know if it's a good idea to use this for learning, instead of learning

> for education Is there any standard curriculum course for... this? (Actually, I don't know if it's a good idea to use this for learning, instead of learning Lean, because I imagine that 95% of learning Lean would be Learning its library anyway. But I never actually tried to use these kind of tools for anything.)