Getting started on a laptop/desktop
The easiest way to get started in Lean 4 is to download Visual Studio code and the Lean 4 extension. This is explained in the following video:
The video is part of a playlist of videos on Lean 4.
Getting started without a laptop/desktop
In case you do not have an appropriate laptop/desktop, you have a few options:
- Use one of the cloud based services: Gitpod or Github Codespaces. The setup is explained in the playlist, except you should start with (your copy of) the course repository.
- Get an account on a machine in the mathematics department with vs-code server setup and connect from a browser. For this contact Siddhartha Gadgil.
Setting up a repository
You will need to set up a private repository for the lab work from the course repository. In addition you will have to set up public repositories for your projects.