Lean as a way to learn proving

Stream: new members

[ashpil]

Hi all,

I'm a CS undergraduate currently enrolled in a couple math classes.

Despite the fact that I never fully properly understood mathematical proofs, I've always enjoyed programming in a very strictly typed environment, and using types to help me reason about my programs. When I learned that theorem provers like Lean use types to prove, I started wondering: can I use my decently good understanding of types to improve my shoddy understanding of proofs? Is this considered a valid use case for Lean, or will I have trouble coming at it from this angle?

Do you guys find that proving something in Lean translates well to proving it on paper? I've compared a couple of paper proofs to Lean proofs and at times the connection was not immediately obvious to me.

Are there resources about Lean that are geared towards people like me as a target audience? That is, CS/programming people trying to use it to learn more math.

Hope those questions made sense. Excited to venture into the world of Lean and proofs!

[Gareth Ma]

I have only done Lean for a short period of time, so the following might not be accurate, but it's my current impression. When I (and you) say Lean, I mean more specifically related to mathlib, which is the maths library by the Lean community.

I think the usual way of using Lean is to translate maths proofs on paper => Lean, not the other way around. You can think of Lean as a more formal language of maths, whereas what we write on paper usually is more casual, i.e. we only write enough to ensure the others understand. The underlying concepts of a proof is still the same, and so people usually find it easier to reason with less vague language than formalising everything. A huge part of Lean proofs are the mathematical ideas underlying anyways.

The part about using types to prove is more like the words in the language, like having alphabets in English or characters in Chinese. There is probably some relation with staticly typed programming (I come from a Rust background too haha), though others probably have a better answer than I do.

So maybe it's not exactly what you want, but I think you should always try and see how you feel!

[Mario Carneiro]

I think a good reference for lean as a gateway to basic logic is #tpil (especially chapter 3). Lean is helpful here because you get immediate feedback on what works and what doesn't, and lean will not let you confuse your forall and exists, and doing some logic puzzles in lean will help you learn the patterns of proof.

[Mario Carneiro]

The natural number game (#nng) is also a popular approach to learning how to use lean and how to do basic proof methods; this one starts off the bat with a small selection of tactics and proves things by rewriting and induction, and using them to build the theory of natural numbers from scratch.

[Anne Baanen]

You might also be interested in Logic and Proof: http://avigad.github.io/logic_and_proof/ The focus is perhaps more on studying logic itself than using it for mathematical proof, but you seem to fit well in its target audience.