### Learning proof with Lean

Seminar

29th April 2019, 2:00 pm – 3:00 pm

Howard House, 4th Floor Seminar Room

In this talk, I will present preliminary findings from a research project concerning a teaching intervention on proof. Much of the advanced mathematics education literature is dedicated to investigating difficulties that first year undergraduate students have with proof. Among these difficulties we have problematic use of formal language, rigour of proof, logical structure of proof, lack of identification of main mathematical objects involved in the proof and they properties. The automated prover Lean (https://leanprover.github.io) was used on a voluntary basis in a first year transition to proof module at Imperial College London. This mixed method study will investigate the impact that the use of Lean had on students’ proof production, and whether the use of such automated prover can help students overcame proving challenges typically described in the education literature.

*Organiser*: Quantum Information Theory Group

*Organisers*: Harry Petyt, Jordan Frost

*Organisers*: Florian Bouyer, Witold Sadowski

*Organiser*: Emilia Alvarez

*Organiser*: Ayalvadi Ganesh

*Organiser*: Karoline Wiesner

*Organiser*: Song Liu

*Organiser*: Nick Jones

*Organisers*: Philip Welch, Philipp Schlicht

*Organisers*: Andrew Booker, Chris Lutsko, Pip Goodman

*Organisers*: Matthew Bisatt, Dan Fretwell, Oleksiy Klurman, Gene Kopp, Min Lee

*Organisers*: Scott Harper, James Williams

*Organisers*: David Ellis, Brendan Murphy

*Organisers*: Thomas Jordan, Rhiannon Dougall, Demi Allen

*Organisers*: Silke Henkes, Shibabrat Naik

*Organisers*: Michiel van den Berg, Kevin Hughes, John Mackay

*Organisers*: Tyler Helmuth, Ofer Busani

## Comments are closed.