This is a typical discrete math course except formalized in Lean 4. The Mechanics of Proof using Lean by Heather MacBeth They may fully mechanize 15-210 soon using calf/decalf to prove costs. 15-210 Parallel & Sequential ALgorithms (SML) Latest version of the book (2022) The hw/labs can be found here or here A very detailed rewrite of the regex matcher from Harper's SML book for proof directed deb