Lean versions and Codewars

Stream: new members

[Martin Dvořák]

Is Codewars good for learning Lean today?

I was playing there a bit, the challenges were fun, but my solutions (written and tested in VS Code) didn't work when I uploaded them to Codewars. It seems that Codewars uses an older version of Lean and/or mathlib. In particular, I was recommended Lean 3.20.0 and this https://github.com/leanprover-community/mathlib/commit/da66bb81bf0466335bae82077f0c335dfe53aeb3 mathlib commit. How much is this obsolete? Will working with that force me to learn things that will be useless for me when working with the current version of Lean and mathlib?

[Eric Rodriguez]

they're not going to be useless, but they're not going to be great either. I'd recommend Kevin's tutorials for further lean learning, or just trying to dive in and do some cool stuff in mathlib ^^

[Martin Dvořák]

Which tutorials do you recommend in particular? I have already done most of the Natural Number Game and most of the Lean tutorials project. I could work on finishing the remaining exercises in these two but I don't find it very rewarding anymore. On the other hand, contributing to mathlib is currently way beyond my level. Is there any tutorial of "medium difficulty" better than Codewars? What do you recommend?