Presentations & Abstracts

Abstract: Since 2019, I have been using Lean to help teach a first-year introduction-to-proof course with a cohort size of 260. This academic year, I used Lean for summative assessments, constituting 10% of the module. I will report on the successes and challenges of this approach, together with my plans for further development.

14:45-15:15 (GMT) Teaching mathematicians to formalise (Prof Kevin Buzzard)

Abstract: In the last year, I have taught a graduate course and a final year undergraduate course, and the goal of each course was to teach students how to formalise mathematics in Lean. I'll give an overview of how things went.

15:15-15:30 (GMT) Break

15:30-16:00 (GMT) Teaching Lean vs. teaching with Lean (Dr Robert Lewis)

Abstract: I have taught two courses at Brown University where students have used Lean: one in which formal verification is the subject of the class, and one (in progress) in which the goal is to teach traditional discrete mathematics. I will compare and contrast my approaches in these two settings and ruminate on what has worked and what hasn't.

16:00-16:30 (GMT) Teaching undergraduate mathematicians and computer scientists how to formalize mathematics (Prof Jeremy Avigad)

Abstract: In the fall of 2023, I taught an undergraduate course on the formalization of mathematics at Carnegie Mellon, targeted to third-year students in mathematics and computer science. In this talk, I will describe the course and reflect on the experience.

16:30-17:00 (GMT) Q & A

Day 2 - 19th April

14:00-14:15 (GMT) Introduction

14:15-14:45 (GMT) Students’ engagement with Lean: working in the Advanced Proposition World of the Natural Number Game (Dr Paola Iannone & Dr Athina Thoma)

Abstract: In this talk, we report on the different ways in which two first-year students engaged with level 4 of the Advanced Proposition World in the Natural Numbers Game. During the interviews, which were video recorded, students shared their screens and used the think aloud protocol while programming in Lean. Here, we analysed the proofs they produces in Lean, we report on their comments on the proofs while they produced them and we highlight the differences between the ways in which the two students think about programming the Lean proofs and the role that they ascribe to the ITP. We conclude with some implication for the use of Lean in undergraduate mathematics teaching.

14:45-15:15 (GMT) Students share their experiences

15:15-15:30 (GMT) Break

15:30-16:00 (GMT) Proving with the Lean theorem prover: The case of transitivity of implication (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.

16:00-16:30 (GMT) A "calculation-heavy" introduction to proof, with support from Lean (Dr Heather Macbeth)

Abstract: I will report on my experience teaching with Lean in an early-undergraduate (1st and 2nd year students) mathematics course: an American intro-to-proof course with an emphasis on concrete numeric examples. The course is genuinely bilingual between English and Lean, with every proof carried out in parallel formally and informally. Substantial custom automation supports proof-writing at the same level of detail as is required of the students on paper, notably in calculational proofs of equalities, inequalities and (modular-arithmetic) congruences.

16:30-17:00 (GMT) Q & A

Day 3 - 20th April

14:00-14:15 (GMT) Introduction

14:15-14:45 (GMT) Using Lean with controlled natural language input to teach mathematical proof writing to first year undergrads (Prof Patrick Massot)

Abstract: In this talk, I will report on my use of Lean to teach how to find and write mathematical proofs. Since January 2019, I am using Lean to teach first year undergrad double major maths/CS students, first alone and then with Frédéric Bourgeois and Christine Paulin. The main mathematical topic of this course is elementary real analysis, especially the theory of convergent sequences and continuous functions. Since 2021, I use a controlled natural language for input in order to facilitate transferring Lean proofs to pen and paper proofs.

14:45-15:15 (GMT) Experiences from a formal verification course designed for 3rd year math majors (Dr Phillip Wood)

Abstract: This semester, I am teaching an introduction to formal verification using Lean to 18 students, with the prerequisite of at least two proof-based mathematics courses previously. The course is heavily based on a similar course taught by Jeremy Avigad at CMU in Fall 2022, and the course closely follows the book Mathematics in Lean. I will discuss some challenges and successes with the course, give a mini-demo of a lecture, and discuss how students are doing with the transition in April from doing weekly homework to working on implementing a final capstone project.