Paola Iannone

Learning proof with Lean

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.