ProofBuddy: How it Started, How it's Going
Nadine Karsten (TU Berlin), Kim Jana Eiken (TU Berlin), Uwe Nestmann (TU Berlin)

TL;DR
ProofBuddy is a web-based proof assistant built on Isabelle, designed to enhance teaching and learning of proofs through interactive tutorials, offering advantages like simplicity, maintainability, and customizability over traditional desktop applications.
Contribution
The paper introduces ProofBuddy, a web application for proof education that demonstrates the benefits of web deployment, including interactive tutorials and improved usability, based on iterative design research.
Findings
Web application offers better maintainability and customization.
Interactive tutorials enhance proof learning experience.
Web deployment provides advantages over desktop tools.
Abstract
We report on our journey to develop ProofBuddy, a web application that is powered by a server-side instance of the proof assistant Isabelle, for the teaching and learning of proofs and proving. The journey started from an attempt to use just Isabelle in an educational context. Along the way, following the educational design research approach with a series of experiments and their evaluations, we observed that a web application like \ProofBuddy has many advantages over a desktop application, for developers and teachers as well as for students. In summary, the advantages cover simplicity, maintainability and customizability. We particularly highlight the latter by exhibiting the potential of interactive tutorials and their implementation within ProofBuddy.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
