NotesFAQContact Us
Collection
Advanced
Search Tips
Publication Date
In 20251
Descriptor
Computer Software1
Learning Processes1
Mathematical Logic1
Mathematics Instruction1
Programming Languages1
Teaching Methods1
Undergraduate Students1
Validity1
Source
International Journal of…1
Author
Gila Hanna1
Xiaoheng Yan1
Publication Type
Journal Articles1
Reports - Descriptive1
Education Level
Higher Education1
Postsecondary Education1
Audience
Teachers1
Location
Laws, Policies, & Programs
Assessments and Surveys
What Works Clearinghouse Rating
Showing one result Save | Export
Using the Lean Interactive Theorem Prover in Undergraduate Mathematics
Peer reviewed Peer reviewed
Direct linkDirect link
Xiaoheng Yan; Gila Hanna – International Journal of Mathematical Education in Science and Technology, 2025
As new technological developments continue to change the educational landscape, it is not an exception in the area of proof and proving. This classroom note introduces the use of one of the trending proofs assistants -- the Lean theorem prover. We first provide a technical account of Lean, then exemplify Lean proofs in propositional logic, number…
Descriptors: Mathematics Instruction, Undergraduate Students, Mathematical Logic, Validity