Category Archives: Learning Lean

Building the non-negative integers from scratch

It’s not actually that hard to build the non-negative integers from scratch in Lean. Let’s call them xnat, because Lean already has an inbuilt nat. The code just looks like this: inductive xnat | zero : xnat | succ : … Continue reading

Posted in Learning Lean | 2 Comments

Rational powers

Lean’s core library has no support for rational or real numbers 😦 They are however in the maths library — or we can just make some fake real numbers and use them instead. — let’s define the real numbers to … Continue reading

Posted in Learning Lean, M1F | Leave a comment

Types

Lean uses something called type theory. This can be a little bit counterintuitive to mathematicians. For example there are lots of different kinds of 7. The core Lean library provides us with the natural number 7 = 7:nat, and the … Continue reading

Posted in Learning Lean | Leave a comment

Jeremy Avigad’s Logic and Proof course

Jeremy Avigad runs a Logic and Proof course at Carnegie Mellon, which uses Lean. He teaches Lean in a methodical way which might be perfect for some people. The link I posted is still a work in progress — I … Continue reading

Posted in Learning Lean | Leave a comment

More easy Lean proofs [difficulty : quite easy]

Pure mathematics is all about proofs, so we have to learn how to do proofs. Let’s start with a super-abstract proof. Let’s just take three random mathematical true/false propositions , and , and let’s say that we know that implies … Continue reading

Posted in Learning Lean | 2 Comments

Proving trivial things with Lean [difficulty : quite easy]

If you want to learn Lean, you can do what I did and read a book and do all the exercises. I had a pdf copy which I would browse through, but if you try this route then I would … Continue reading

Posted in Learning Lean | Leave a comment