Introduction to Lean¶
These pages were written for the Lean Together meeting and the target audience is mathematicians with no Lean experience at all. Watch the video and then get started on the exercises.
Which bits could I explain better? What else do you need to be told in order to get going? Let me (Buzzard) know! Thanks to David Holmes and Paula Neeley for comments.
Brief intro video¶
This brief video might be helpful if you want to get started on the exercises.
Tactic guide¶
Need some basic hints about which tactics to use? Try this basic tactic guide or maybe you just want to look at a list of basic tactics.
Glossary¶
A glossary of basic words and phrases is here. This is still very light. What am I missing?
Exercises¶
To get started with these exercises, either run them online in the Lean Web Editor (maybe problems with firefox currently?) or download the Lean files directly and run them locally.
- Sheet 1 – basic propositional logic.
Lean web editor link to sheet 1.
- Sheet 2 – forall, exists, and so on.
Lean web editor link to sheet 2.
- Sheet 3 – defining your own structure I : the natural numbers.
I should write a .lean file, but until then here’s a Link to a blog post about doing this in Lean.
- Sheet 4 – defining your own structure II : the complex numbers.
Here we import the reals from mathlib and then attempt to make a working copy of the complex numbers.