Search papers, labs, and topics across Lattice.
The paper introduces Hazel Prover, a classroom proof assistant designed to enhance students' understanding of equational and inductive reasoning while addressing common deployment challenges in educational settings. Through iterative design and evaluation across two classes, the authors found that while initial iterations provided excessive support, leading to poor transfer to pen-and-paper proofs, subsequent adjustments that increased manual engagement improved students' ability to apply learned concepts independently. The findings highlight the importance of balancing assistance with student autonomy to facilitate effective learning and knowledge transfer in mathematical proofs.
Students using Hazel Prover showed significant improvement in inductive reasoning, but initial excessive support hindered their ability to transfer skills to traditional assessments.
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.
