Learning Mathematics with LEAN

  • 6 April 2022
  • 10:30-16:15
  • Loughborough University campus - room to be confirmed

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 

Book now

Contact and booking details

Name
Paola Iannone
Telephone number
+44 (0) 1509 225 903
Email address
p.iannone@lboro.ac.uk
Booking required?
Yes
Booking information
Registration for this event has closed. If you wish to attend please contact Paola Iannone.