Proof Assistants for Teaching: a Survey
Fr\'ed\'eric Tran Minh (Universit\'e Grenoble-Alpes, Grenoble INP, LCIS, France), Laure Gonnord (Universit\'e Grenoble-Alpes, Grenoble INP, LCIS, France), Julien Narboux (IRIF, Universit\'e Paris Cit\'e, CNRS, Paris, France)

TL;DR
This survey reviews how proof assistants are increasingly used in education, highlighting experimental applications, adaptations, and interface improvements for teaching logic, mathematics, and computer science.
Contribution
It provides a comprehensive overview of existing educational tools and adaptations of proof assistants for teaching purposes, summarizing prior experimental and design efforts.
Findings
Proof assistants are effectively used in teaching logic and mathematics.
Various adaptations improve user interfaces for educational use.
Educational proof systems support undergraduate learning.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
