# ProofBuddy: A Proof Assistant for Learning and Monitoring

arXiv: https://arxiv.org/abs/2308.06970 · HTML: https://mlsanity.com/paper/2308.06970/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Aug 2023.

## Built on by (most cited first, 2 of 2)

- [LeanTutor: Towards a Verified AI Mathematical Proof Tutor](https://mlsanity.com/paper/2506.08321/) (2025)
- [LeanTutor: Towards a Verified AI Mathematical Proof Tutor](https://mlsanity.com/paper/2601.17473/) (2026)

## Abstract (arXiv)

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.