使用Lean定理证明器教授《数学基础》
Teaching "Foundations of Mathematics" with the Lean Theorem Prover
AI总结：
本研究以苏黎世大学大一《数学基础》课程学生为对象开展试点，通过访谈与期末成绩分析，结合t检验、Mann-Whitney U检验，探究Lean定理证明器对学生数学证明理解的积极影响。
摘要：
本研究旨在观察定理证明器Lean是否对学生理解数学证明产生积极影响。为此，我们在苏黎世大学（UZH）的大一学生中开展了一项试点研究。研究过程中，我们采用了特定的教学方法，并从选修《数学基础》课程的志愿学生中收集数据。经过11周的学习（内容涵盖部分用Lean实现的练习题），我们将使用Lean的学生与未接触Lean的其他学生进行对比，衡量前者在证明数学命题方面的表现。为进行这项衡量，我们访谈了5名使用Lean的学生和4名未使用Lean的学生，并分析了所有学生的期末考试成绩。最后，我们通过独立样本t检验和Mann-Whitney U检验来验证结果的显著性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
