Hazel Prover: A Classroom Proof Assistant for Learning Structural Induction

• URL: http://arxiv.org/abs/2608.23309v1
• Date: Mon, 24 Aug 2026 14:29:41 GMT
• Title: Hazel Prover: A Classroom Proof Assistant for Learning Structural Induction
• Abstract summary: Hazel Prover is a classroom proof assistant for teaching equational and inductive reasoning.<n>We present a design informed by criteria encompassing ease-of-use of the tool, student engagement with underlying mathematical ideas, transfer to pen-and-paper proof, and classroom logistics.<n>Our analysis demonstrates that students were able to learn to use the tool effectively, and that students became more capable with inductive proof as they progressed through problems.
• Score: 0.7733046964560364
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Proof assistants offer instant feedback and incremental proof scaffolding to users. Both of these features have long held promise in improving mathematics education in classroom settings, where manual grading is costly, and students often struggle with knowing how to proceed in their proof. However, they have been difficult to deploy in classroom settings due to two main concerns: (i) students struggle with the intricacies of full-scale proof assistants; and (ii) proof assistants are ineffective in support of student learning, and knowledge transfer to on-paper assessments without the tool. We present Hazel Prover, a classroom proof assistant for teaching equational and inductive reasoning, with a design informed by criteria encompassing ease-of-use of the tool, student engagement with underlying mathematical ideas, transfer to pen-and-paper proof, and classroom logistics. We synthesized these criteria from observations made in prior deployments of proof assistants to the classroom. We engaged in an iterative design and evaluation process, deploying Hazel Prover in two different classes and conducting in-depth analyses of fine-grained usage logs, survey data, and student exam responses. Our analysis demonstrates that students were able to learn to use the tool effectively, and that students became more capable with inductive proof as they progressed through problems. However, the first design did not effectively achieve transfer to pen-and-paper proofs. We hypothesized that this was due to the tool offering too much help to students in the equational reasoning steps. Based on this negative result, we enforced more manual student engagement with equational steps, which led to more effective transfer in the second deployment. We believe that our analyses offer generalizable insights relevant to the designers of future classroom proof assistants for a variety of mathematical domains.

Related papers

• AgentBrew: Lifelong Knowledge Brewing from Strong Teachers to Weak LLM Agents [8.847692192802343]
  LLM agents typically require a compact test-time student, even if a stronger teacher is available during training.<n>This setting poses two challenges: environments provide only sparse, binary feedback, and teacher-authored notes must be inherently tailored to be concretely executable by a substantially weaker student.<n>We propose AgentBrew, comprising two coupled components. First, a failure-triggered teacher--Ralph Loops sparse feedback by transforming student failures into environment-validated notes.<n>Second, student-aware synthesis calibrates teacher knowledge to the weak executor's operational granularity, yielding model-specific, actionable guidance.
  arXiv  Detail & Related papers  (2026-07-18T15:23:45Z)
• Alice: Proactive Learning with Teacher's Demonstrations for Weak-to-Strong Generalization [69.96794098855938]
  Weak-to-strong generalization (W2SG) offers a promising framework for supervising increasingly capable language models (LLMs)<n>Traditional W2SG methods rely on passive learning, where a weak teacher provides noisy demonstrations to train a strong student.<n>We introduce Alice, a framework that leverages complementary knowledge between teacher and student to enhance the learning process.
  arXiv  Detail & Related papers  (2025-04-09T22:33:06Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  We introduce LeanProgress, a method that predicts the progress in the proof.<n>Our experiments show that LeanProgress achieves an overall prediction accuracy of 75.1%.
  arXiv  Detail & Related papers  (2025-02-25T07:46:36Z)
• Autograding Mathematical Induction Proofs with Natural Language Processing [0.12289361708127876]
  We present a set of training methods and models capable of autograding freeform mathematical proofs.<n>The models are trained using proof data collected from four different proof by induction problems.<n>We recruit human graders to grade the same proofs as the training data, and find that the best grading model is also more accurate than most human graders.
  arXiv  Detail & Related papers  (2024-06-11T15:30:26Z)
• Representational Alignment Supports Effective Machine Teaching [81.19197059407121]
  GRADE is a new controlled experimental setting to study pedagogy and representational alignment.<n>We find that improved representational alignment with a student improves student learning outcomes.<n>However, this effect is moderated by the size and representational diversity of the class being taught.
  arXiv  Detail & Related papers  (2024-06-06T17:48:24Z)
• 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)
• Can Language Models Teach Weaker Agents? Teacher Explanations Improve Students via Personalization [84.86241161706911]
  We show that teacher LLMs can indeed intervene on student reasoning to improve their performance. We also demonstrate that in multi-turn interactions, teacher explanations generalize and learn from explained data. We verify that misaligned teachers can lower student performance to random chance by intentionally misleading them.
  arXiv  Detail & Related papers  (2023-06-15T17:27:20Z)
• Distantly-Supervised Named Entity Recognition with Adaptive Teacher Learning and Fine-grained Student Ensemble [56.705249154629264]
  Self-training teacher-student frameworks are proposed to improve the robustness of NER models. In this paper, we propose an adaptive teacher learning comprised of two teacher-student networks. Fine-grained student ensemble updates each fragment of the teacher model with a temporal moving average of the corresponding fragment of the student, which enhances consistent predictions on each model fragment against noise.
  arXiv  Detail & Related papers  (2022-12-13T12:14:09Z)
• Computationally Identifying Funneling and Focusing Questions in Classroom Discourse [24.279653100481863]
  We propose the task of computationally detecting funneling and focusing questions in classroom discourse. We release an annotated dataset of 2,348 teacher utterances labeled for funneling and focusing questions, or neither. Our best model, a supervised RoBERTa model fine-tuned on our dataset, has a strong linear correlation of.76 with human expert labels and with positive educational outcomes.
  arXiv  Detail & Related papers  (2022-07-08T01:28:29Z)
• ProtoTransformer: A Meta-Learning Approach to Providing Student Feedback [54.142719510638614]
  In this paper, we frame the problem of providing feedback as few-shot classification. A meta-learner adapts to give feedback to student code on a new programming question from just a few examples by instructors. Our approach was successfully deployed to deliver feedback to 16,000 student exam-solutions in a programming course offered by a tier 1 university.
  arXiv  Detail & Related papers  (2021-07-23T22:41:28Z)
• Proof Blocks: Autogradable Scaffolding Activities for Learning to Write Proofs [0.4588028371034407]
  Proof Blocks is a software tool which enables students to write proofs by dragging and dropping prewritten proof lines into the correct order. These proofs can be graded completely automatically, enabling students to receive rapid feedback on how they are doing with their proofs. When constructing a problem, the instructor specifies the dependency graph of the lines of the proof, so that any correct arrangement of the lines can receive full credit.
  arXiv  Detail & Related papers  (2021-06-07T17:03:58Z)

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.