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.