[Previous]

motivations

 [Next]

 
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

 

 
[Previous]

JFLA 2004 — F. GUILHOT

 [Next]