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. Our results show that while the two ITPs can support the development of proof skills, they also present usability challenges - - such as complex syntax and unclear error messaging - - that can hinder learning. We also find that formalized ITP proofs tend to be more explicit and verbose than pen-and-paper proofs, which can affect students' perception of proof difficulty. Our heuristic evaluation highlights specific areas for improvement in Coq and Lean, including clearer error messages, support for example-driven learning, and expanding proof libraries to better align with educational needs. Together, these findings provide actionable insights for instructors considering ITPs for education and highlight both the pedagogical benefits and current limitations of these systems, as well as opportunities for researchers to improve ITPs as educational tools.