Item request has been placed! ×
Item request cannot be made. ×
loading  Processing Request

Proof assistants for undergraduate mathematics education: elements of an a priori analysis

Item request has been placed! ×
Item request cannot be made. ×
loading   Processing Request
Read More Add to Saved list
  • Additional Information
    • Contributors:
      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)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg); Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-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 - CNRS Chimie (INC-CNRS)-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 - CNRS Chimie (INC-CNRS)-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); UFR Mathématique et Informatique Strasbourg (UNISTRA UFR MI); Université de Strasbourg (UNISTRA)-Université de Strasbourg (UNISTRA)
    • Publication Information:
      HAL CCSD
    • Publication Date:
      2023
    • Collection:
      École des Ponts ParisTech: HAL
    • 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.
    • Online Access:
      https://hal.science/hal-04087080
      https://hal.science/hal-04087080v1/document
      https://hal.science/hal-04087080v1/file/PA_apriori_long-submitted.pdf
    • Rights:
      http://hal.archives-ouvertes.fr/licences/copyright/ ; info:eu-repo/semantics/OpenAccess
    • Accession Number:
      edsbas.3994889