Proof Assistants for Teaching: a Survey

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.