Toward the use of a proof assistant to teach mathematics - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2005

Toward the use of a proof assistant to teach mathematics

Résumé

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.
Fichier principal
Vignette du fichier
RP_Narboux.pdf (172.09 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

inria-00495952 , version 1 (01-07-2010)

Identifiants

  • HAL Id : inria-00495952 , version 1

Citer

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. ⟨inria-00495952⟩
174 Consultations
356 Téléchargements

Partager

Gmail Facebook X LinkedIn More