[zant]

Hey this is really cool. I want to start doing the same thing.

Visual group theory is a really nice book for intuition. Also, the YouTube series "Essence of Group Theory" can help in this same line.

What I also want to do while self learning is formalizing some theorems and definitions in Lean. Even just looking at how they're already defined in mathlib [1] can be of great help when internalizing the concepts.

https://github.com/leanprover-community/mathlib/blob/292e3fa...

[jimsimmons]

Side question: what do you think of Lean? I’m not sure what people who know this stuff think of it. I’ve read comments that say Lean is inferior to OCaml and it simply hyped by celebrity

[zant]

Yeah a lot of people is shadowing Lean and labeling the success as some sort of marketing success.

I digress from this opinion, mainly because I believe that what truly makes Lean shine is not the language itself but what's around it.

I see Lean as something of a Rust in some aspects. It's a relatively young language, created with a good user experience in mind and a really good environment around it: starting from the VSCode integration, Web support, well written documentation, increasing learning resources and great community. It's just so easy to get started and learn.

At the end there are a lot of other options such as Coq, Isabelle, Agda and others. However, what's around the language is in my opinion more important than specific design decision, and this may be part of the current Lean success.

[jimsimmons]

Interesting perspective. Thanks