Mathematics interface supports learning and expert proof automation
Proof Interfaces for Exploratory Mathematics
Programming Languages
Summary
People often use pen and paper or whiteboards to work through math problems and proofs, but this can lead to mistakes and unclear reasoning. The authors created a flexible computer interface that helps both students and expert mathematicians by offering different levels of math automation and detailed explanations. Students get more step-by-step guidance while experts can automate many steps, making proofs faster and more reliable. The system also lets experts export their proofs to a formal theorem prover to increase precision. The authors show examples from basic to college-level math to demonstrate the interface’s usefulness.
What this means in practice
- •For educational software developers: Create interactive math learning tools that provide step-by-step proof explanations and automation tuned to different skill levels.$Commercial implications: The paper enables educational product companies to build adaptive math tutors that support detailed proof walkthroughs for students.
- •For software engineers in formal methods: Integrate user-friendly proof interfaces with formal theorem provers to improve proof creation and verification workflows for experts.
Authors
Nishant Kheterpal, Matthew Keenan, Cyrus Omar, Jean-Baptiste Jeannin
Abstract
This paper describes a mathematics interface intended for both educational applications and exploratory mathematics. Both learners and mathematics practitioners often use pen and paper or a whiteboard to perform equational reasoning, manipulate expressions, or construct proofs. These workflows lead to a variety of problems: transcription errors, tedious writing and notation, and/or unclear standards for proof justification. We extend the Hazel Prover, an equational-reasoning interface in the Hazel live programming environment, to add capabilities for exploratory mathematics, with varying levels of verbosity and automation aimed at both students and expert users. Students require more deliberate practice when learning mathematical concepts and correspondingly more verbose justifications, while experts may benefit from significant mathematical automation. With this in mind, our interface supports multiple levels of mathematical automation and simplification, grounded in a rewrite search architecture. For expert users, motivated by a gap in the accessibility of formal methods, we support proof export to the Rocq theorem prover, extending this rewrite search to proof tactics. This paper closes with several case studies covering elementary- to college-level mathematics.