Papers With

← All papers
First page of Proof Assistants for Teaching: a Survey

Proof Assistants for Teaching: a Survey

Frédéric Tran Minh, Laure Gonnord, Julien Narboux

cs.LO May 9, 2025 · v1 cs.HC
meta-study tooling
Read PDF arXiv abstract
TL;DR
Surveys educational uses of proof assistants, covering Lean-based courses and Lean teaching tools such as Deaduction, Paperproof, ProofWidgets and the Lean 4 web editor.
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.
Problem

Proof assistants are increasingly used in education, but the reported teaching experiments and educational adaptations are scattered across the literature. The survey collects prior work on using proof assistants for mostly undergraduate teaching.

Approach

It reviews teaching experiments with Mizar, Coq, Isabelle, Lean and other systems in logic, mathematics and computer science. It also covers tutoring systems and proof assistants designed for education, including geometry provers. It discusses interface adaptations of general-purpose provers, such as web editors, proof-tree displays and proof-by-pointing. Finally, it covers controlled natural-language input and natural-language output of proofs. Lean material includes courses using Lean 3 and Lean 4, the Deaduction front-end, Paperproof and ProofWidgets.

(d) Paperproof.
(f) A proof that injective applications preserve intersection in Deaduction.
Results

Proof assistants for teaching are diverse in design, proof language, interaction mode, proof visualization and student feedback. Teaching material is widespread in logic and software foundations. Didactic evaluation of these tools, especially for mathematics teaching, is still at an early stage.