# 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

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

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

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

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

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

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