Proof Assistants for Teaching: a Survey
In parallel to the ever-growing usage of mechanized proofs in diverse areas of mathematics and computer science, proof assistants are used more and more for education.This paper surveys previous work related to the use of proof assistants for (mostly undergraduate) teaching.This includes works where the authors report on their experiments using proof assistants to teach logic, mathematics or computer science, as well as designs or adaptations of proof assistants for teaching.We provide an overview of both tutoring systems that have been designed for teaching proof and proving, or general-purpose proof assistants that have been adapted for education, adding user interfaces and/or dedicated input or output languages.
Authors
- Julien Narboux (ORCID: https://orcid.org/0000-0003-3527-7184)
- gonnord Laure Danthony
- Frédéric Tran Minh (ORCID: https://orcid.org/0009-0003-9221-5585)
Institutions
- Institut polytechnique de Grenoble (FR)
- École Normale Supérieure de Lyon (FR)
- Centre National de la Recherche Scientifique (FR)
- Université Paris Cité (FR)
- Sorbonne Paris Cité (FR)
- Laboratoire des Sciences de l'Ingénieur, de l'Informatique et de l'Imagerie (FR)
- Institut de Recherche en Informatique Fondamentale (FR)
- Laboratoire de l'Informatique du Parallélisme (FR)
- Laboratoire de Conception et d'Intégration des Systèmes (FR)
- Université Grenoble Alpes (FR)
Publication Details
- Journal
- Electronic Proceedings in Theoretical Computer Science
- Published
- 2025-05-07
- DOI
- https://doi.org/10.4204/eptcs.419.1
- Citations
- 4
- Primary Topic
- Logic, programming, and type systems
- Type
- article
- Field-Weighted Citation Impact
- 9.92
Funders
- Agence Nationale de la Recherche