NotesFAQContact Us
Collection
Advanced
Search Tips
Showing all 6 results 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
Interactive Theorem Provers for University Mathematics: An Exploratory Study of Students' Perceptions
Peer reviewed Peer reviewed
Direct linkDirect link
Paola Iannone; Athina Thoma – International Journal of Mathematical Education in Science and Technology, 2024
Programming is becoming increasingly common in mathematics degrees as it is a desirable skill for new graduates. However, research shows that its use is mostly restricted to computational or modelling tasks. This paper reports a study on students' perceptions of and difficulties with Lean, an interactive theorem prover introduced as part of a…
Descriptors: Programming, Mathematics Instruction, Computer Science Education, Student Attitudes
Combining Building Block Process with Computational Thinking Improves Learning Outcomes of Python Programming with Peer Assessment
Peer reviewed Peer reviewed
Direct linkDirect link
Tsung-Chih Hsiao; Ya-Hsueh Chuang; Chien-Yun Chang; Tzer-Long Chen; Hong-Bo Zhang; Jhih-Chung Chang – SAGE Open, 2023
The capability of computer programming language logic is one of the basics of technical education. How to improve students "interest in program logic design and help overcome students" fears of coding has become vital for educators. Cultivating practical talents with information technology application and basic programming development…
Descriptors: Computer Science Education, Computation, Thinking Skills, Programming
Learning about Proof with the Theorem Prover LEAN: The Abundant Numbers Task
Peer reviewed Peer reviewed
Direct linkDirect link
Thoma, Athina; Iannone, Paola – International Journal of Research in Undergraduate Mathematics Education, 2022
This exploratory study reports on characteristics of proof production and proof writing observed in the work of first-year university students who took part in workshops on the theorem prover LEAN (https://leanprover.github.io). These workshops were voluntary and offered alongside a transition to proof module in a UK university. Through…
Descriptors: Validity, Mathematical Logic, Mathematics Instruction, Undergraduate Students
Using Computer Programming as an Effective Complement to Mathematics Education: Experimenting with the Standards for Mathematics Practice in a Multidisciplinary Environment for Teaching and Learning with Technology in the 21st Century
Peer reviewed Peer reviewed
Direct linkDirect link
Solin, Pavel; Roanes-Lozano, Eugenio – International Journal for Technology in Mathematics Education, 2020
Many mathematics educators are not aware of a strong connection that exists between the education of computer programming and mathematics. The reason may be that they have not been exposed to computer programming. This connection is worth exploring, given the current trends of automation and Industry 4.0. Therefore, in this paper we take a closer…
Descriptors: Computer Science Education, Mathematics Education, Programming Languages, Interdisciplinary Approach
What They Learn When They Learn Coding: Investigating Cognitive Domains and Computer Programming Knowledge in Young Children
Peer reviewed Peer reviewed
Direct linkDirect link
Strawhacker, Amanda; Bers, Marina Umaschi – Educational Technology Research and Development, 2019
Computer programming for young children has grown in popularity among both educators and product developers, but still relatively little is known about what skills children are developing when they code. This study investigated N = 57 Kindergarten through second grade children's performance on a programming assessment after engaging in a 6-week…
Descriptors: Coding, Programming, Computer Science Education, Kindergarten