AI 中文总结
本研究提出Hazel Prover课堂证明助手，经两次班级部署与分析，发现调整工具对等式推理步骤的帮助程度可提升学生向纸笔证明的知识迁移效果，为相关工具设计提供可推广见解。
AI 中文摘要
证明助手可为用户提供即时反馈与增量式证明支架，这两项特性长期以来有望改善课堂场景中的数学教育——在课堂中人工评分成本高昂，学生常不知如何推进证明。但受两个主要问题制约，证明助手难以在课堂部署：其一，学生难以掌握全规模证明助手的复杂细节；其二，证明助手对学生学习的支持不足，无法将知识迁移至无工具的纸笔评估场景。我们提出Hazel Prover，一款用于教授等式推理与归纳推理的课堂证明助手，其设计基于易用性、学生对底层数学概念的参与度、向纸笔证明的迁移性及课堂后勤保障等标准，这些标准源自此前证明助手课堂部署的观察结果。我们开展迭代设计与评估流程，将Hazel Prover部署至两个不同班级，对细粒度使用日志、调查数据及学生考试作答进行深入分析。分析表明，学生能够有效学习使用该工具，且随问题推进，学生的归纳证明能力有所提升。但首次设计未能有效实现向纸笔证明的迁移，我们假设这是由于工具在等式推理步骤中为学生提供了过多帮助。基于该负面结果，我们要求学生在等式步骤中进行更多手动参与，这在第二次部署中实现了更有效的迁移。我们认为，本研究的分析可为未来面向各类数学领域的课堂证明助手设计者提供可推广的见解。
英文摘要
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.
