Conférence IREM : vers l'utilisation d'un assistant de preuve en classe ?

Julien Narboux, maître de conférences à l'UFR de mathématique et informatique et membre de l'équipe Informatique Géométrique et Graphique au laboratoire ICube, animera une conférence le mercredi 12 décembre 2018 à 14h30. Cette dernière se déroulera dans le petit amphi de mathématiques (PAM) de l'UFR Math-Info de Strasbourg.

Résumé : A l'heure actuelle les logiciels populaires utilisés en classe en mathématique servent à calculer numériquement, calculer symboliquement, visualiser, expérimenter, conjecturer, mais pas à raisonner ni à démontrer.

Les assistants de preuve comme Coq, Isabelle, HOL-Light sont des logiciels permettant de vérifier des démonstrations mathématiques.
Ils sont utilisés à la fois pour vérifier des théorèmes purement mathématiques (théorème des quatre couleurs, théorème de Hales, théorème de Feit-Thompson, ...) et pour vérifier des systèmes informatiques (logiciel de pilotage d'une ligne de métro, compilateur, ...). Nous pensons que l'utilisation d'un assistant de preuve en classe pourrait aider les élèves à acquérir des compétences concernant le raisonnement logique, et la rédaction de démonstrations.

Cet exposé présentera d'abord une vue d'ensemble du domaine de la preuve formelle, puis je montrerai comment un assistant de preuve peut être utilisé en classe pour enseigner le concept de démonstration.
Je montrerai des exemples en utilisant la plateforme Edukera:
- Niveau 3ième: résolution d'équations du premier degré,
- Niveau Ts: preuves par récurrence, suites. On évoquera les questions suivantes:

• Qu’est-ce qu’un assistant de preuve ?
• Quelle est la différence entre une preuve informelle et formelle ?
• Peut-on produire des preuves formelles ?
• Pourquoi utiliser un assistant de preuve en classe ?