### 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

*Organisers*: Emilia Alvarez, Pip Goodman

*Organiser*: Ayalvadi Ganesh

*Organiser*: Karoline Wiesner

*Organiser*: Mathieu Gerber

*Organiser*: Nick Jones

*Organisers*: Philip Welch, Philipp Schlicht

*Organisers*: Andrew Booker, Kirsti Biggs, Chris Lutsko

*Organisers*: Catherine Hsu, Min Lee, Jonathan Bober, Matthew Bisatt

*Organisers*: Ben Barrett, Radhika Gupta, Alex Malcolm, Leonid Monin

*Organisers*: Kevin Grace, David Ellis, Brendan Murphy

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

*Organisers*: John Russo, Aurore Loisy

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

*Organisers*: Tyler Helmuth, Ofer Busani

## Comments are closed.