1. Proof assistants for undergraduate mathematics education: elements of an a priori analysis
- Author
-
Bartzia, Evmorfia-Iro, Beffara, Emmanuel, Meyer, Antoine, Narboux, Julien, Laboratoire Alexander Grothendieck (LAG), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), Modèles et Technologies pour l’Apprentissage Humain (MeTAH ), Laboratoire d'Informatique de Grenoble (LIG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), Institut de Recherche sur l’Enseignement des Mathématiques [Grenoble] (IREM), Laboratoire d'Informatique Gaspard-Monge (LIGM), École des Ponts ParisTech (ENPC)-Centre National de la Recherche Scientifique (CNRS)-Université Gustave Eiffel, IREM de Paris, Université Paris Cité (UPCité), Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (ICube), École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et Nanosciences Grand-Est (MNGE), Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Réseau nanophotonique et optique, Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), Institut de Recherche sur l'Enseigment des Mathématiques [Strasbourg] (IREM), Université de Strasbourg - UFR Mathématique et Informatique (UNISTRA UFR MI), and Université de Strasbourg (UNISTRA)-Université de Strasbourg (UNISTRA)
- Subjects
logic ,Didactics of University Mathematics ,teaching proof ,computer assisted theorem proving ,proof ,proof assistant ,reasoning ,[INFO.EIAH]Computer Science [cs]/Technology for Human Learning ,[INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS] - Abstract
This paper presents an a priori analysis of the use of six different interactive proof assistants for education, based on the resolution of a typical undergraduate exercise on abstract functions. It proposes to analyze these tools according to three main categories of aspects: language and interaction mode, automation and user assistance, and proof structure and visualization. We argue that this analysis may help formulate and clarify further research questions on the possible impact of such tools on the development of reasoning and proving skills.
- Published
- 2023