### Categories

# 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