FMitF: Track III: Customizing a Classroom Proof Assistant for Mathematical Computing and Engineering Courses

Students are typically taught to derive equational proofs by hand, with little or no direct feedback or mechanical assistance during the process. The project’s novelties are the development of a customizable classroom proof assistant, called the Hazel Prover, that provides classroom-appropriate automated assistance and feedback to students as they derive equational proofs. The project’s impacts are the development, deployment, and evaluation of customized instances of the Hazel Prover into a representative sample of courses offered at all levels in the College of Engineering at the University of Michigan that collectively enroll several thousand students per year. With the aid of these tools, students benefit from a much tighter and more accurate feedback loop, improving learning. The technology and course material, which are made broadly available to researchers and instructors, advance the fields of educational technology and automated theorem prover design. The project addresses several challenges that have limited the impact of existing proof assistants in the classroom. In particular, modern proof assistants (1) present an excessively steep learning curve, particularly in courses where programming is not a prerequisite, (2) require shifting from conventional and domain-specific mathematical notation to textual programming notation, (3) are intolerant of errors, unlike human graders, and (4) are distractingly pedantic, requiring users to satisfy proof obligations that humans typically elide. The proposed research refines and deploys a customizable classroom proof assistant, the Hazel Prover, that solves or can be customized to solve each of these problems. The Hazel Prover builds incrementally on the recent work by the investigator on the Hazel educational programming environment, including promising preliminary work on the Hazel Stepper tool that has already been deployed successfully into the classroom. The system interfaces with the Coq theorem prover and existing math proof libraries, while only exposing students to structured easy-to-use proof construction affordances. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.