ProofBuddy: How it Started, How it's Going

• URL: http://arxiv.org/abs/2505.13474v1
• Date: Fri, 09 May 2025 12:18:32 GMT
• Title: ProofBuddy: How it Started, How it's Going
• Authors: Nadine Karsten, Kim Jana Eiken, Uwe Nestmann,
• Abstract summary: We report on our journey to develop ProofBuddy, a web application that is powered by a server-side instance of the proof assistant Isabelle.<n>The advantages cover simplicity, maintainability and customizability.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• The "Huh?" Button: Improving Understanding in Educational Videos with Large Language Models [7.237493755167876]
  We propose a simple way to use large language models (LLMs) in education.<n>Specifically, our method aims to improve individual comprehension by adding a novel feature to online videos.
  arXiv  Detail & Related papers  (2024-12-15T21:02:16Z)
• ProofBuddy: A Proof Assistant for Learning and Monitoring [0.0]
  Proof competence, i.e. the ability to write and check (mathematical) proofs, is an important skill in Computer Science. 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. We have performed a preliminary usability study of ProofBuddy at the Technical University of Denmark.
  arXiv  Detail & Related papers  (2023-08-14T07:08:55Z)
• Exploring the Benefits of Visual Prompting in Differential Privacy [54.56619360046841]
  Visual Prompting (VP) is an emerging and powerful technique that allows sample-efficient adaptation to downstream tasks by engineering a well-trained frozen source model. We explore and integrate VP into canonical DP training methods and demonstrate its simplicity and efficiency.
  arXiv  Detail & Related papers  (2023-03-22T01:01:14Z)
• Active Teacher for Semi-Supervised Object Detection [80.10937030195228]
  We propose a novel algorithm called Active Teacher for semi-supervised object detection (SSOD) Active Teacher extends the teacher-student framework to an iterative version, where the label set is partially and gradually augmented by evaluating three key factors of unlabeled examples. With this design, Active Teacher can maximize the effect of limited label information while improving the quality of pseudo-labels.
  arXiv  Detail & Related papers  (2023-03-15T03:59:27Z)
• On Exams with the Isabelle Proof Assistant [0.0]
  We present an approach for testing student learning outcomes in a course on automated reasoning using the Isabelle proof assistant. The approach allows us to test both general understanding of formal proofs in various logical proof systems and understanding of proofs in the higher-order logic of Isabelle/HOL.
  arXiv  Detail & Related papers  (2023-03-10T11:37:09Z)
• Dodona: learn to code with a virtual co-teacher that supports active learning [0.0]
  Dodona is an intelligent tutoring system for computer programming. It provides real-time data and feedback to help students learn better. The source code of Dodona is available on GitHub under the permissive open-source license.
  arXiv  Detail & Related papers  (2022-10-19T16:56:11Z)
• Benchopt: Reproducible, efficient and collaborative optimization benchmarks [67.29240500171532]
  Benchopt is a framework to automate, reproduce and publish optimization benchmarks in machine learning. Benchopt simplifies benchmarking for the community by providing an off-the-shelf tool for running, sharing and extending experiments.
  arXiv  Detail & Related papers  (2022-06-27T16:19:24Z)
• Multi-Task Learning based Online Dialogic Instruction Detection with Pre-trained Language Models [34.66425105076059]
  We propose a multi-task paradigm which enhances the ability to distinguish instances of different classes by enlarging the margin between categories via contrastive loss. Experiments on a real-world online educational data set demonstrate that our approach achieves superior performance compared to representative baselines.
  arXiv  Detail & Related papers  (2021-07-15T04:57:57Z)
• Visual Transformer for Task-aware Active Learning [49.903358393660724]
  We present a novel pipeline for pool-based Active Learning. Our method exploits accessible unlabelled examples during training to estimate their co-relation with the labelled examples. Visual Transformer models non-local visual concept dependency between labelled and unlabelled examples.
  arXiv  Detail & Related papers  (2021-06-07T17:13:59Z)
• Privileged Knowledge Distillation for Online Action Detection [114.5213840651675]
  Online Action Detection (OAD) in videos is proposed as a per-frame labeling task to address the real-time prediction tasks. This paper presents a novel learning-with-privileged based framework for online action detection where the future frames only observable at the training stages are considered as a form of privileged information.
  arXiv  Detail & Related papers  (2020-11-18T08:52:15Z)
• Beyond Language: Learning Commonsense from Images for Reasoning [78.33934895163736]
  This paper proposes a novel approach to learn commonsense from images, instead of limited raw texts or costly constructed knowledge bases. Our motivation comes from the fact that an image is worth a thousand words, where richer scene information could be leveraged to help distill the commonsense knowledge.
  arXiv  Detail & Related papers  (2020-10-10T13:47:13Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.