ProofBuddy: A Proof Assistant for Learning and Monitoring

TL;DR

ProofBuddy is a web-based proof assistant tool designed to enhance learning and monitoring of proof competence in students, enabling detailed data collection for educational research.

Contribution

This paper introduces ProofBuddy, a novel web-based proof assistant built on Isabelle, facilitating research on proof learning and assessment.

Findings

Preliminary usability study conducted at DTU

ProofBuddy effectively collects detailed student interaction data

Initial positive feedback on usability and potential educational benefits

Abstract

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.