Show simple item record

dc.contributor.authorHanna, Gila
dc.contributor.authorLarvor, Brendan
dc.contributor.authorYan, Xiaoheng
dc.date.accessioned2023-09-20T14:15:00Z
dc.date.available2023-09-20T14:15:00Z
dc.date.issued2023-02-02
dc.identifier.citationHanna , G , Larvor , B & Yan , X 2023 , ' Human-Machine Collaboration in the Teaching of Proof ' , Journal of Humanistic Mathematics , vol. 13 , no. 1 , pp. 99-117 . https://doi.org/10.5642/jhummath.AZEV3747
dc.identifier.issn2159-8118
dc.identifier.otherORCID: /0000-0003-0921-1659/work/142859993
dc.identifier.urihttp://hdl.handle.net/2299/26705
dc.description©2023 by the authors. This is an open access article distributed under the terms of the Creative Commons Attribution License (CC BY), https://creativecommons.org/licenses/by/4.0/
dc.description.abstractThis 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.en
dc.format.extent18
dc.format.extent967777
dc.language.isoeng
dc.relation.ispartofJournal of Humanistic Mathematics
dc.subjectProof
dc.subjectLean
dc.subjectMathematics
dc.subjectTeaching
dc.subjectEducation
dc.titleHuman-Machine Collaboration in the Teaching of Proofen
dc.contributor.institutionPhilosophy
dc.contributor.institutionSchool of Creative Arts
dc.description.statusPeer reviewed
rioxxterms.versionofrecord10.5642/jhummath.AZEV3747
rioxxterms.typeJournal Article/Review
herts.preservation.rarelyaccessedtrue


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record