ProofBuddy: A Proof Assistant for Learning and Monitoring

Nadine Karsten
(Technische Universität Berlin)
Frederik Krogsdal Jacobsen
(Technical University of Denmark)
Kim Jana Eiken
(Technische Universität Berlin)
Uwe Nestmann
(Technische Universität Berlin)
Jørgen Villadsen
(Technical University of Denmark)

Proof competence, i.e. the ability to write and check (mathematical) proofs, is an important skill in Computer Science, but for many students it represents a difficult challenge. The main issues are the correct use of formal language and the ascertainment of whether proofs, especially the students' own, are complete and correct. Many authors have suggested using proof assistants to assist in teaching proof competence, but the efficacy of the approach is unclear. To improve the state of affairs, we introduce ProofBuddy: a web-based tool using the Isabelle proof assistant which enables researchers to conduct studies of the efficacy of approaches to using proof assistants in education by collecting fine-grained data about the way students interact with proof assistants. We have performed a preliminary usability study of ProofBuddy at the Technical University of Denmark.

In Elena Machkasova: Proceedings Twelfth International Workshop on Trends in Functional Programming in Education (TFPIE 2023), Boston, Massachusetts, USA, 12th January 2023, Electronic Proceedings in Theoretical Computer Science 382, pp. 1–21.
Published: 14th August 2023.

ArXived at: https://dx.doi.org/10.4204/EPTCS.382.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org