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.
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.
In my personal experience, I find extremely difficult to stick with the courses that are mostly video based. Not just from OCW but Coursera, edX, etc.
But what I found is that, for me, a really good way to start learning a new subject is studying from Lecture Notes.
These are generally less dense and more tractable than a whole textbook, and at the same time, you get the written form which I find a bit easier to follow than multiple hours of video.
Of course you miss the depth in some cases, but as introductory content I find them really to the point and easing the learning curve.
I strongly agree on this one. As a programmer and someone who's always been interested in mathematics, having a way to check proofs without relying on trust of my own logic or a third agent, but solely on a prover like Lean or Coq is a really big difference.
Yeah you can say that. You can also say that Machine Learning is just programming. Or in a similar way you can also say that First Order Logic is just programming.
However, the cool thing about programming is that it lets us represent a lot of different things. In this case you're representing the construction and interaction of mathematical objects, with a language that targets a specific proof management system to verify this constructions.
But yes, it is "just programming", and some functional languages even support proofs to some extent like Scala or Agda.
I absolutely love everything about this. Specially how it can provide access to knowledge to people all around the world.
I'm currently thinking about getting a degree in Maths, and I find extremely appealing the notion of having a repo of knowledge from where to gather theorems, specially useful for newer developed areas.
I would add self-enhancement to this. I recently started to exercise with rings and go on deeper math, and every progress is very rewarding. I think this apply to anything one may choose.
There's also a good one made by Grant Sanderson from 3blue1brown. This video was the first time I was introduced to the concept and had no trouble following it: https://www.youtube.com/watch?v=8rrHTtUzyZA
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.