Toward the use of a proof assistant to teach mathematics

Abstract : Proof is a crucial aspect of mathematics and must have a prominent role in the education. Dynamic Geometry Software (D.G.S.) and Computer Algebra Software (C.A.S) are widely used in a pedagogical context. These tools are used to explore, visualize, calculate, find counter examples, conjectures, or check facts, but most of them can not be used to build a proof in itself. But there are software whose sole purpose is to help the user produce proofs : the proof assistants. We believe that proof assistants are now mature enough to be adapted to the education. After giving a quick overview of what a proof assistant is, we will discuss the possible advantages of using it in the education. Finally we report on the ongoing work to ease the use of a proof assistant in the classroom.
Type de document :
Communication dans un congrès
The Seventh International Conference on Technology in Mathematics Teaching (ICTMT7), Jul 2005, Bristol, United Kingdom. 2005
Liste complète des métadonnées

https://hal.inria.fr/inria-00495952
Contributeur : Julien Narboux <>
Soumis le : jeudi 1 juillet 2010 - 14:07:14
Dernière modification le : jeudi 11 janvier 2018 - 06:19:44
Document(s) archivé(s) le : lundi 4 octobre 2010 - 11:43:36

Fichier

RP_Narboux.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00495952, version 1

Collections

Citation

Julien Narboux. Toward the use of a proof assistant to teach mathematics. The Seventh International Conference on Technology in Mathematics Teaching (ICTMT7), Jul 2005, Bristol, United Kingdom. 2005. 〈inria-00495952〉

Partager

Métriques

Consultations de la notice

154

Téléchargements de fichiers

185