Teaching "Foundations of Mathematics" with the Lean Theorem Prover
Mattia Luciano Bottoni, Alberto S. Cattaneo, Elif Sacikara
math.HO
Jan 6, 2025 · v1
TL;DR
Studies whether teaching with the Lean theorem prover improves university students' understanding of mathematical proving.
Abstract
This study aims to observe if the theorem prover Lean positively influences students' understanding of mathematical proving. To this end, we perform a pilot study concerning freshmen students at the University of Zurich (UZH). While doing so, we apply certain teaching methods and gather data from the volunteer students enrolled in the ``Foundations of Mathematics'' course. After eleven weeks of study covering some exercise questions implemented with Lean, we measure Lean students' performances in proving mathematical statements, compared to other students who are not engaged with Lean. For this measurement, we interview five Lean and four Non-Lean students and we analyze the scores of all students in the final exam. Finally, we check significance by performing a $t$-test for independent samples and the Mann-Whitney $U$-test.
Problem
It is unclear whether interactive theorem provers like Lean can positively influence undergraduate students' understanding of mathematical proof, and no controlled study has been conducted on this question.
Approach
The authors conducted a pilot study with freshmen at the University of Zurich in the Foundations of Mathematics course. Five volunteer students used Lean alongside the course for eleven weeks, while four control students did not. Teaching methods included weekly sessions with Lean-implemented exercises. Performance was measured via interviews and final exam scores, with significance tested using t-tests and Mann-Whitney U-tests.
Results
The study gathered qualitative interview data from 9 students and quantitative exam scores from all enrolled students. Statistical tests (t-test for independent samples and Mann-Whitney U-test) were applied to compare Lean and non-Lean student performance on proving mathematical statements in the final exam.
