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 believe his course is running right now and some things aren’t quite finished, or need certain libraries which may or may not be installed by default — but the course certainly contains some very illustrative examples of how to use Lean to do some basic mathematics.

Note that this is a course running in a computer science department, so there is more emphasis on things like the lambda calculus than one would normally see in a mathematics course. On the other hand I am well aware that some readers of this blog are on a joint mathematics and computer science degree…

### Like this:

Like Loading...

*Related*

## About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.