Back to Search
Start Over
Human-Machine Collaboration in the Teaching of Proof.
- Source :
- Journal of Humanistic Mathematics; Jan2023, Vol. 13 Issue 1, p99-117, 19p
- Publication Year :
- 2023
-
Abstract
- This paper argues that interactive theorem provers (ITPs) could play an important role in fostering students' appreciation and understanding of proof and of mathematics in general. It shows that the ITP Lean has three features that mitigate existing difficulties in teaching and learning mathematical proof. One is that it requires students to identify a proof strategy at the start. The second is that it gives students instant feedback while still allowing them to explore with maximum autonomy. The third is that elementary formal logic finds a natural place in the activity of creating proofs. The challenge in using Lean is that students have to learn its command language, in addition to mathematics course content and elementary logic. [ABSTRACT FROM AUTHOR]
- Subjects :
- MATHEMATICAL proofs
MATHEMATICS
LOGIC
Subjects
Details
- Language :
- English
- ISSN :
- 21598118
- Volume :
- 13
- Issue :
- 1
- Database :
- Complementary Index
- Journal :
- Journal of Humanistic Mathematics
- Publication Type :
- Academic Journal
- Accession number :
- 162608040
- Full Text :
- https://doi.org/10.5642/jhummath.azev3747