Installing Lean

All the software we will use in this course, including Lean and its main library, are free and open source. With this comes a familiar speedbump: community-developed software is not always the easiest to install. Luckily, the Lean community has put in some effort to streamline the process.

You will need the following:

The course staff will be available at the beginning of the course to help with installation hiccups.

Note: when you open VSCode, be sure to open a full Lean project. That means, use File -> Open Folder... to open a folder that contains a leanpkg.toml file (e.g., the fpv2022 directory). Alternatively, open VS Code from the command line with code fpv2022.

If you open a single file instead of a directory, the Lean VSCode plugin will not know what version of Lean to use, and your imports will most likely not work.

Course Files

The lecture notes, practice exercises, and homework assignments will be uploaded to the course GitHub repository: We recommend cloning this repository now and periodically pulling as we update and add files over the course of the semester.