|
Coq et
l'enseignement des mathématiques
- Coq
formalisation de théories mathématiques
preuves construites interactivement (logique)
- enseignement
du raisonnement déductif
cours de géométrie dans le secondaire
=> bibliothèque de
géométrie en Coq dédiée
à l'enseignement
contraintes
fortes
- formalisation
définitions, théorèmes et démonstrations
"comme au lycée"
- accessibilité
réduire
la distance entre texte formel et texte naturel
production de figures
|
|