The goal of this project is to quickly teach you how to use Lean for mathematics using a very hands-on approach. It can be used alongside Theorem proving in Lean or independently. You can first play the Natural number game first, but this is not mandatory.
Currently, those tutorials do no cover creating your own theories, only
proving things in elementary real analysis. All exercices are adapted
from a first year undergraduate course by Patrick Massot in Orsay,
adding only explanations about compressing proofs using slightly advanced
tactics like rintros and rcases.
What you do need first is to install Lean and get this project for local use by typing:
leanproject get tutorials
Then, in the src folder, create a copy of the exercises folder for you work.
This way it won't be overwritten if you update the project to get new exercices.
You can then open the tutorials folder in VS code. The first file
00_first_proofs.lean does not contain any exercise, it is meant as an
overview of the basics. You can skip it if you are really eager to start
coding, but this is not recommended. You don't need to understand
everything while reading this file, only try to get a feel for what it's
looking like, and maybe start picking up some key words.
There are solutions for all the exercises in src/solutions. If you
need help about any specific exercise. You can come on
Zulip in the "new members" stream
and look for a thread called "tutorials NNNN" where NNNN is the exercise
number. If no such thread exists, you can create one!