Teaching Lean vs. teaching with Lean

Part of the "Learning Mathematics with Lean-2nd Event" sites.google.c...
Title: Teaching Lean vs. teaching with Lean
Speaker: Dr Robert Lewis
Abstract: I have taught two courses at Brown University where students have used Lean: one in which formal verification is the subject of the class, and one (in progress) in which the goal is to teach traditional discrete mathematics. I will compare and contrast my approaches in these two settings and ruminate on what has worked and what hasn't.