Proving with the Lean theorem prover: The case of transitivity of implication

Part of the "Learning Mathematics with Lean-2nd Event" sites.google.c...
Title: Proving with the Lean theorem prover: The case of transitivity of implication
Speakers: Dr Kitty Yan & Prof Gila Hanna
Abstract: As universities are starting to introduce the Lean theorem prover in a number of mathematics courses at the undergraduate level, it is becoming essential to examine how students use Lean. In this presentation, we report how three undergraduate students used Lean to prove the transitivity of implication after they attended a Lean workshop. We identify learning patterns that students exhibit, and describe both successes and challenges they encountered. One key finding of the study is that the students’ approaches to proving the transitivity of implication greatly varied. This suggests that proving with Lean could offer a balance between rigor and accessibility and between autonomy and control, while allowing students to construct different yet equally valid proofs.