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

*Organisers*: Luke Jeffreys, Irene Pasquinelli

*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*: Henry Reeve

*Organiser*: Thomas Bothner

*Organisers*: Philip Welch, In collaboration with Oxford Set Theory Seminar

*Organisers*: Andrew Booker, Ayesha Hussain, Simone Muselli

*Organisers*: Samuel Edwards, Dan Fretwell, Oleksiy Klurman, Min Lee, Sam Streeter

*Organiser*: Scott Harper

*Organisers*: David Ellis, Brendan Murphy

*Organisers*: Thomas Jordan, Henna Koivusalo

*Organisers*: Silke Henkes, Shibabrat Naik

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

*Organisers*: Benjamin Lees, Jessica Jay

## Comments are closed.