Proof Assistants for Teaching: a Survey

TL;DR

This survey maps the landscape of proof assistants in education, detailing teaching experiments, tool specialization, interface innovations, and natural-language interfaces. It highlights how Coq, Lean, Isabelle, and other systems have been adapted for classroom use, from logic and meta-theory to undergraduate mathematics and geometry, and it addresses the crucial issue of feedback quality and proof granularity. The authors synthesize evidence on educational impact, noting the lack of systematic comparative studies while identifying design criteria and practical approaches that may improve learning outcomes. The work underscores a growing, multi-faceted ecosystem where teaching-focused tooling, user interfaces, and natural-language representations aim to make formal proofs more accessible and pedagogically effective, with optimism for broader adoption in the coming years.

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.

Figures (7)

• Figure 1: Logic games
• Figure 2: Geometry software featuring not only proof verification, but also tutoring.
• Figure 3: Proof visualizations.
• Figure 4: Proof by pointing.
• Figure 5: Natural Language Output