Awesome

lean 4 tutorials

The goal of this project is to quickly teach you how to use Lean 4 for mathematics using a very hands-on approach. It can be used alongside Theorem proving in Lean 4 or independently.

Currently, these tutorials do not cover creating your own theories, only proving things in elementary real analysis. All exercises 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 4 and get this project. [todo: add instructions]

Then, in the Tutorials4/Tutorials 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 exercises. You can then open the tutorials folder in VS code. For instance you can type:

cp -r tutorials4/Tutorials/Exercises tutorials4/Tutorials/MyExercises
code tutorials4

VSCode has a file explorer that you can open by clicking the top icon in the icon column on the left. In this explorer, you can navigate to Tutorials/MyExercises and click on 00FirstProofs.lean. This file 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 Tutorials/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 "tutorials4 NNNN" where NNNN is the exercise number. If no such thread exists, you can create one!