Learning Mathematics with LEAN
This workshop is funded by the London Mathematical Society (LMS).
Join us at Loughborough University for a workshop about using the automated theorem prover Lean (https://leanprover.github.io) to teach first year pure mathematics. Speakers will talk about their experiences of using Lean for teaching and the resources they created. There will also be the opportunity for hands-on sessions to try some of resources designed for students. You can join the workshop here at Loughborough or online - but the hands-on sessions will not be streamed. If you plan to come in person bring your laptop with you!
Programme:
10:30 - 11:00 - Arrival and coffee
11:00 - 11:30 - Fools rush in: how not to insert theorem provers into a curriculum - Prof. Kevin Buzzard, Imperial College, London
11:30 - 11:50 - Lean Games - Dr Gihan Marasingha, University of Exeter
11:50 - 12:30 - Playing with Lean Games (Hands-on session)
12:30 - 13:10 - Undergraduate students share their experiences
13:10 - 13:50 - Lunch
13:50 - 14:15 - Research on students’ use of Lean - Dr Paola Iannone, Loughborough University & Dr Athina Thoma, University of Southampton
14:15 - 14:45 - Teaching with Lean - Prof Jeremy Avigad, Carnegie Mellon University, US
14:45 - 15:00 - Coffee break
15:00 - 16:00 - Programming on Lean (Hands-on session)
16:00 - 16:15 - Q&A and closing
Contact and booking details
- Name
- Paola Iannone
- Telephone number
- +44 (0) 1509 225 903
- Email address
- p.iannone@lboro.ac.uk
- Booking information
- Registration for this event has closed. If you wish to attend please contact Paola Iannone.