Teaching "Foundations of Mathematics" with the Lean Theorem Prover

TL;DR

This study investigates whether using the Lean theorem prover enhances freshmen's ability to construct mathematical proofs in a Foundations of Mathematics course. It combines a 11-week Lean-based teaching intervention with five Lean and four Non-Lean student groups, interviews, and final-exam analysis, evaluating significance via $t$-tests for independent samples and the Mann-Whitney $U$-test. Findings show no significant difference in interview-based assessments but a statistically significant Lean advantage in final-exam performance, with qualitative notes on improved proof structure and motivation alongside implementation challenges and curriculum integration considerations. The work contributes empirical guidance on Lean-enabled pedagogy, highlighting potential benefits, limits, and hybrid approaches for incorporating proof assistants into undergraduate mathematics education.

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.

Figures (34)

• Figure 1: The Lean interface in VS Code with the helpful infoview on the right side.
• Figure 2: Error-message when trying to exact $hP$ from the example above.
• Figure 3: A suggestion for the next step generated by GitHub Copilot.
• Figure 4: Using the intro tactic to prove that $P \Rightarrow P$ holds for any proposition.
• Figure 5: Using the exact tactic concludes the proof that $P \Rightarrow P$ holds for any proposition.