Schedule

14:00 - 14:10 (GMT) Introduction

14:15 - 14:45 (GMT) Assessing mathematical understanding using Lean for a large cohort of first-year mathematics undergraduates Dr Gihan Marasingha

14:45 - 15:15 (GMT) Teaching Mathematicians to formalise Prof Kevin Buzzard

15:15-15:30 (GMT) Break

15:30 - 16:00 (GMT) Teaching Lean vs. teaching with Lean Dr Robert Lewis

16:00 - 16:30 (GMT) Teaching undergraduate mathematicians and computer scientists how to formalize mathematics Prof Jeremy Avigad

16:30 - 17:00 (GMT) Q&A

14:00 - 14:10 (GMT) Introduction

14:15 - 14:45 (GMT) Students' engagement with Lean: working in the Advanced Proposition World of the Natural Number Game Dr Paola Iannone & Dr Athina Thoma

14:45 - 15:15 (GMT) Students share their experiences

15:15-15:30 (GMT) Break

15:30 - 16:00 (GMT) Proving with the Lean theorem prover: The case of transitivity of implication Dr Kitty Yan & Prof Gila Hanna

16:00 - 16:30 (GMT) A "calculation-heavy" introduction to proof, with support from Lean Dr Heather Macbeth

16:30 - 17:00 (GMT) Q&A

14:00 - 14:10 (GMT) Introduction 

14:15 - 14:45 (GMT) Using Lean with controlled natural language input to teach mathematical proof writing to first year undergrads Prof Patrick Massot

14:45 - 15:15 (GMT) Experiences from a formal verification course designed for 3rd year math majors Dr Phillip Wood

15:15-15:30 (GMT) Break

15:30 - 16:30 (GMT) Students share their experiences 

16:30 - 17:00 (GMT) Q&A