### 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, Daniel Berlyne

*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, Kentaro Fujimoto, Philipp Schlicht

*Organisers*: Andrew Booker, Michael Farmer-Evans, Andrei Seymour-Howell

*Organisers*: Oleksiy Klurman, Min Lee, Ross Paterson, Sam Streeter

*Organisers*: Tim Burness, Charles Cox

*Organisers*: David Ellis, Tom Johnston

*Organisers*: Thomas Jordan, Henna Koivusalo, Laura Monk

*Organiser*: Rachel Bennett

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

*Organisers*: Benjamin Lees, Jessica Jay

## Comments are closed.