ProofBuddy—How it Started, How it's Going—

We report on our journey to develop PROOFBUDDY, a web application that is powered by a serverside 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.* Our tool PROOFBUDDY should not be confused with another tool called "Proof Buddy" [8].We first presented an extended abstract about PROOFBUDDY [16] in

Authors

Institutions

Publication Details

Journal
Electronic Proceedings in Theoretical Computer Science
Published
2025-05-07
DOI
https://doi.org/10.4204/eptcs.419.6
Primary Topic
Logic, programming, and type systems
Type
article
Field-Weighted Citation Impact
0.00
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

ProofBuddy—How it Started, How it's Going—

Uwe Nestmann, Nadine Karsten, Kim Jana Eiken
Electronic Proceedings in Theoretical Computer Science
Logic, programming, and type systems
article

ProofBuddy—How it Started, How it's Going—

Uwe Nestmann, Nadine Karsten, Kim Jana Eiken
article en

Abstract

We report on our journey to develop PROOFBUDDY, a web application that is powered by a serverside 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.* Our tool PROOFBUDDY should not be confused with another tool called "Proof Buddy" [8].We first presented an extended abstract about PROOFBUDDY [16] in

Electronic Proceedings in Theoretical Computer ScienceVol. 419
Technische Universität Berlin (DE)
Openalex Percentile: Top 96%
Logic, programming, and type systems
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.