Beginner to abstract math getting started with Lean

Stream: new members

[Andrew Lubrino]

I'm a beginner to math and a beginner to Lean. I work in an industry that requires some mathematical and technological sophistication, but nothing beyond applied linear algebra or building small programs using Python. I'm interested in learning abstract math and I stumbled across the book at this link, which introduces abstract math with the Lean software. This seems like an interesting option, but I want to make sure I know what I'm getting into. I've tried learning this kind of thing from books, but I find it very hard to do so when there is no one to verify the proof I've written. Even if a book had full solutions (and I haven't come across one that does), I'd imagine that my proof might be different than the author's and I'd want to know that my proof was correct. Lean would be a feedback system that could help me learn the material without a teacher. Is Lean a terrible place for me to start learning abstract math? I've linked a book above. Are there solutions out there to the exercises that the reader is supposed to solve on pen and paper? Thanks!!

[Kevin Buzzard]

My experience with teaching lean to students is that it's best to learn the abstract maths first and then to learn how to do it in lean. In particular I am not convinced that using lean to learn abstract maths is a viable idea for a beginner. But this is just my experience.

[Stuart Presnell]

If you’re going to use Lean to help you learn some mathematics, it’s important to note that the code in the mathlib library is written in a very terse condensed style and is not intended to be easy to read. So if you click into one of the definitions or lemmas and find a knot of cryptic code, please don’t get the impression that this is what all Lean code looks like!

[Chris B]

Andrew Lubrino said:

I'd want to know that my proof was correct. Lean would be a feedback system that could help me learn the material without a teacher. Is Lean a terrible place for me to start learning abstract math?

Lean will definitely tell you whether or not your proof is correct; depending on the problem it may or may not be a good way to get feedback that feels like help with a math problem. Just to push back a little bit on what Kevin said, if you don't have a math background and aren't in a setting where you can consult peers or professors, I think the biggest difficulty in getting some momentum is that it can be very difficult to concretize ideas you're reading in a book or paper, which is something proof assistants are actually pretty good at.

[Stuart Presnell]

@Andrew Lubrino Do you know about Kevin's course from the start of this year? All the notes are exercises are available from here:
https://github.com/ImperialCollegeLondon/formalising-mathematics

[Arthur Paulino]

From personal experience, learning Lean's syntax (which I still haven't learned completely) and getting used to what's already in mathlib (tactics and lemmas, which I still haven't got the hang of either) is being a difficult task in itself

[Arthur Paulino]

I would try to aid my difficulty on acknowledging the validity of my proofs some more. Are you trying to grasp undergrad math? MSc level math? PhD level math? Which field of mathematics are you most interested in?

[Andrew Lubrino]

Wow. I want to thank everyone for the responses. I apologize for responding so late here. I didn't even realize I was getting responses on the platform. It seems like opinions are mixed here. I get the feeling that most think it would be difficult to learn Lean and abstract math at the same time, but I haven't been successful learning abstract math in any other way, so I think it's worth a shot. I will ask the community for help as need. Thanks again for all the input.

[Stuart Presnell]

Remember that you don’t have to be learning Lean and new mathematics at the same time. I’d highly recommend working through the courses linked earlier in this thread to get a basic understanding of Lean before you try to use it in learning new topics in mathematics.

[Stuart Presnell]

Kevin’s course contains material that you may not be familiar with, such as topology and filters, although it’s not intended as a comprehensive introduction to those topics.

[Kevin Buzzard]

My course was specifically designed for people who knew no lean but who knew the relevant mathematics well (they were math PhD students)

[Andrew Lubrino]

Yes, I looked at Kevin's course. The material there is way over my head. The course I linked in my original post here starts with deductive logic, then moves to sets, and then to other important fundamental topics along with number theory. It also moves back and forth between pen and paper proofs and Lean. I actually like this approach a lot, and there are places I can learn Lean, but I wanted to know if there were solutions floating around anywhere for that book (the book is linked on the Lean website).