Course notes and supplemental materials will be added here as the semester progresses.
General references
Lean documentation: logic, quantifiers, induction, and recursion
Class materials
Day 1 — Discussion of Proof and AI: Computers in mathematics, 1956–2026 · Proposition 0.39 · Sudoku
Day 2 — August 24: Sudoku
Day 3: macros.lean · day03-nosoln.lean · day03-soln.lean
Day 4: day04-nosoln.lean · day04-soln.lean
Day 5: day05-nosoln.lean · day05-soln.lean
Day 6: day06-nosoln.lean · day06-soln.lean
Day 7: quiz01a-nosoln.pdf · quiz01a-soln.pdf · quiz01b-nosoln.pdf · quiz01a-soln.pdf
Day 9: grids.pdf
Day 10: day10-nosoln.lean · day10-soln.lean
Day 11: day11-nosoln.lean · day11-soln.lean
Day 12: day12-nosoln.lean · day12-soln.lean
Day 14: day14-nosoln.lean · day14-soln.lean
Day 17: Induction: day17-nosoln.lean · day17-soln.lean
Day 18: Induction: day18-nosoln.lean · day18-soln.lean
Day 20: Induction: day20-nosoln.lean · day20-soln.lean
Day 22: Class Lean project