Fiche du document
5 juillet 2023
- handle: 10670/1.yhqf4f
- hal: hal-04227823
Mots-clés
proof assistant teaching foundations Teaching proofSujets proches
ProofCiter ce document
Evmorfia-Iro Bartzia et al., « Underlying theories of proof assistants and potential impact on the teaching and learning of proof », HALSHS : archive ouverte en Sciences de l’Homme et de la Société, ID : 10670/1.yhqf4f
Métriques
Partage / Export
Résumé
Proof assistants (or PA) are computer programs which allow users to describe mathematical objects, express properties of these objects in a formal language, interactively construct formal proofs of these properties and algorithmically check these proofs’ validity. PAs have been used in research for decades, and are now also increasingly used in education, to support the teaching and learning of proof. In this talk, based on an a-priori epistemological analysis of PAs and actual task examples and teaching experiments, we will investigate how the underlying theoretical foundations of proof assistants may interact with students’ learning and teachers’ objectives at undergraduate level.