← Course home

Course notes and supplemental materials will be added here as the semester progresses.

General references

Logical operators in Lean

Introduction and elimination rules in Lean

OneDrive notes folder

Online Lean compiler

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