Lecture slides and lecture notes are regularly posted at the Piazza website for CS 511 (only accessible to students registered for the course) and as the semester progresses, typically early in the week in which they are presented. On this webpage, only headings of topics covered every week will be listed.

• Week 1:

• Week 2:

• Week 3:

• Week 4:

• Week 5:

• Week 6:

• Week 7:

• Week 8:

• Week 9:

• Week 10:

• Week 11:

• Week 12:

• Week 13:

• Week 14:

The main reading material will be lecture notes by the instructor, all downloadable from the Piazza website for CS 511. In addition to lecture notes, we will use external references:

For Lean 4, we will use the books under Books in the leanprover-community website, here listed in order of increasing depth and presumed mathematical sophistication : 

The Mechanics of Proof , by Heather Macbeth. 

Theorem Proving in Lean 4 , by J. Avigad, L. de Moura, S. Kong and S. Ullrich.

Mathematics in Lean, by J. Avigad and P. Massot.

For topics in mathematical logic complementing the lecture notes, we will use:

Logic and Proof , by J. Avigad, J. Hua, R. Lewis, and F. van Doorn.  The web version is available here, which is based on the older version available here, which uses Lean 3.