A "calculation-heavy" introduction to proof, with support from Lean

Part of the "Learning Mathematics with Lean-2nd Event" sites.google.c...
Title: A "calculation-heavy" introduction to proof, with support from Lean
Speaker: Dr Heather Macbeth
Abstract: I will report on my experience teaching with Lean in an early-undergraduate (1st and 2nd year students) mathematics course: an American intro-to-proof course with an emphasis on concrete numeric examples. The course is genuinely bilingual between English and Lean, with every proof carried out in parallel formally and informally. Substantial custom automation supports proof-writing at the same level of detail as is required of the students on paper, notably in calculational proofs of equalities, inequalities and (modular-arithmetic) congruences.