Interactive Theorem Provers for Proof Education

Proof techniques are a core component of computer science (CS) education, yet many CS students struggle to engage with and understand proof-based material. Interactive Theorem Provers (ITPs), originally developed for formal verification, have emerged as promising educational tools that offer structured feedback and align well with CS students’ existing technical skills. While recent work has begun to explore the use of ITPs in educational settings, a notable gap remains: little is known about how well these tools support the range of proof techniques taught in CS curricula or how they might be improved to do so. We specifically seek to close this gap and contribute to the growing literature on ITPs in education through three concrete efforts: a user study of student experiences with the Coq proof assistant, a case study comparing proof development across Coq, Lean, and traditional methods, and a heuristic evaluation of each ITP using Nielsen’s usability heuristics.