A glimpse of Lean
This repository is an introduction to theorem proving in Lean for the impatient.
The goal is to get a feel for what proving in Lean looks like in 2 or 3 hours.
After reading the Introduction.lean file, you should read explanations and do exercises in the
Basics folder, and then choose to work on one file from the Topics folder.
Of course you can play with all files from that folder if you have more time.
If you have a lot more time, you should read the book Mathematics in Lean (but note that book is currently using the stable version of Lean, Lean 3, whereas this repository uses the brand new Lean 4 which is not yet fully ready for mathematical use).
