Category Archives: Learning Lean

Working with integers

The integers. Lean has integers inbuilt as part of the core library. You can call them int if you want to be old skool, but if you type \Z (and then hit the space bar) in VS Code or emacs … Continue reading

Posted in Learning Lean | Leave a comment

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 | 3 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