Teaching "Foundations of Mathematics" with the Lean Theorem Prover
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909454898823168 |
|---|---|
| author | Bottoni, Mattia Luciano Cattaneo, Alberto S. Sacikara, Elif |
| author_facet | Bottoni, Mattia Luciano Cattaneo, Alberto S. Sacikara, Elif |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_03352 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Teaching "Foundations of Mathematics" with the Lean Theorem Prover Bottoni, Mattia Luciano Cattaneo, Alberto S. Sacikara, Elif History and Overview 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. |
| title | Teaching "Foundations of Mathematics" with the Lean Theorem Prover |
| topic | History and Overview |
| url | https://arxiv.org/abs/2501.03352 |