ERIC Number: EJ1450642
Record Type: Journal
Publication Date: 2024-Dec
Pages: 13
Abstractor: As Provided
ISBN: N/A
ISSN: ISSN-1863-9690
EISSN: EISSN-1863-9704
Using the Proof Assistant Lean in Undergraduate Mathematics Classrooms
Gila Hanna; Brendan Larvor; Xiaoheng Kitty Yan
ZDM: Mathematics Education, v56 n7 p1517-1529 2024
In this paper we develop a case for introducing a new teaching tool to undergraduate mathematics. Lean is an interactive theorem prover that instantly checks the correctness of every step and provides immediate feedback. Teaching with Lean might present a challenge, in that students must write their proofs in a formal way using a specific syntax. Accordingly, this paper addresses the issue of formalism from both a theoretical and a practical point of view. First, we examine the nature of proof, referring to historical and contemporary debates on formalization, and then show that in mathematical practice there is a growing rapprochement between strictly formal proof and proofs-in-practice. Next, we look at selections from the mathematics education literature that discuss how and when students advance through higher levels of mathematical maturity to reach a point at which they can cope with the demands of rigorous formalism. To probe the integration of Lean into teaching from an empirical point of view, we conducted an exploratory study that investigated how three undergraduate students approached the proof of double negation with Lean. The findings suggest that the rigorous nature of Lean is not an obstacle for students and does not stifle students' creativity in writing proofs. On the contrary, proving with Lean offers a great deal of flexibility, allowing students to follow different paths to creating a valid proof.
Descriptors: Undergraduate Study, College Mathematics, Teaching Methods, Feedback (Response), Validity, Mathematical Logic, Mathematics Instruction, Undergraduate Students, Programming
Springer. Available from: Springer Nature. One New York Plaza, Suite 4600, New York, NY 10004. Tel: 800-777-4643; Tel: 212-460-1500; Fax: 212-460-1700; e-mail: customerservice@springernature.com; Web site: https://bibliotheek.ehb.be:2123/
Publication Type: Journal Articles; Reports - Research
Education Level: Higher Education; Postsecondary Education
Audience: N/A
Language: English
Sponsor: N/A
Authoring Institution: N/A
Grant or Contract Numbers: N/A