Book

We will follow The Hitchhiker’s Guide to Logical Verification by Jasmin Blanchette, et al.

Required software

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:

  • git (likely installed if you are using Linux or OSX; if you’re on Windows, the Lean installation instructions below include instructions for this)
  • Python 3 (again: if you’re on Windows, follow the instructions below)
  • a “regular install” of Lean (these directions will install a version manager called elan, which is what you want)
  • Visual Studio Code and its Lean extension (the Lean installation directions will get you this too)
    • If you prefer emacs to VSCode, there is a [lean-mode] for that too. Just don’t ask Rob for help with it ;)

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 fpv2021 directory). Alternatively, open VSCode from the command line with code fpv2021.

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: https://github.com/BrownCS1951x/fpv2021

Mathlib documentation

The official library documentation refers to the current version of mathlib. To avoid things breaking in the middle of the course because of library changes, we’re using a fixed version of mathlib from this summer. For the most part, the contents are the same, but just in case, we’ve hosted our own copy of the documentation for the version of the library we’re using.

Additional Course Materials

There are lots of materials online that are useful additional resources.

Assignment Submission and Discussion

We will use Ed for course discussions and Gradescope for assignment submissions. Check out the details on our Google doc. (This is only accessible with a Brown account. Get in touch if you need us to give you access!)

Feedback

This is the first time that this course will be taught at Brown. We very strongly encourage feedback on all aspects of the course: the textbook, classes, exercises, homeworks, projects, and more! Please contact the course staff with any feedback—positive or negative, big or small—or use the anonymous report form here.

Inclusion and Support

We welcome students of all backgrounds in this course. We hope to create a supportive environment for everyone to partake in the joys of proof writing. To this end all assignments in this course will be anonymously graded. We will not tolerate any instances of harassment in this course including but not limited to mockery of people’s technical or mathematical talents.

If you feel the TAs have been unprofessional in any way, please contact Professor Rob Lewis. You may also wish to talk to someone outside of course staff in which case you can reach out the department chair.

We recognize that being a student is not easy and wish to provide support however we can. Beyond our staff, here are some resources that are available to you here at Brown: