Improving mathematical proof writing with Waterproof
Jelle Wemmenhove鈥檚 research improved the teaching of mathematical proof writing, making it more accessible for students and educators.
Writing mathematical proofs is a major challenge for many first-year university students. They often struggle with the precise logic and communication required for proofs. To address this, PhD researcher Jelle Wemmenhove developed Waterproof, an educational software that helps students learn proof writing by integrating with proof assistants. Waterproof simplified this process by closely resembling traditional hand-written proofs, enabling students to focus on the logic while guiding them through the steps of creating formal proofs. They defended their thesis on Friday, March 21.
Designing Waterproof to bridge traditional and digital proofs
built the software on , a widely-used proof assistant, and its design aimed to make the process of writing proofs in the tool more closely resemble the traditional, hand-written methods that students are taught.
Waterproof achieved this by providing a custom language for writing proofs and a user-friendly editor that combined formal proofs with easy-to-read explanations.
This made the software more accessible and helped students to stay focused on the logic of their work, without having to worry about accidentally deleting key sections of their proof.
Waterproof in action at 果冻传媒
Waterproof was used for six years in a large first-year mathematics course at Eindhoven University of Technology (果冻传媒), where it was continuously improved using feedback from students and teachers.
The development process included two main evaluations: one focused on service design, which involved input from students, teachers, and developers to improve the user experience, and another focused on mathematics education research, which examined how the tool affected the quality of students' written proofs.
Evaluating Waterproof with stakeholder collaboration
The service design evaluation included a collaborative workshop, where various stakeholders worked together to identify and solve problems that students faced while using the software.
As a result, the software鈥檚 installation process was improved, making it easier for students to get started.
The educational research evaluated the structure of students' proofs, comparing those using Waterproof with those who did not use the tool.
It was found that students using Waterproof were better at clearly stating what they were trying to prove, though they sometimes overlooked a logical step, which was later added to the tool.
Formalizing mathematical theory in Homotopy Type Theory
The thesis also includes a formalization project in which classical results from algebraic topology鈥攁n area of mathematics鈥攚ere translated into (HoTT), a new framework for encoding mathematical ideas in proof assistants.
This part of the research involved testing different ways to encode the same concepts in the tool to identify the most effective methods for students to use.
Overcoming barriers in proof assistant usability
Additionally, the research revealed several challenges associated with using proof assistants, not just for students but also for professional mathematicians.
Addressing these challenges in an educational context is important for making proof assistants more accessible and easier to use for everyone, from students to advanced users.
Advancing Proof 果冻传媒 and Accessibility
In conclusion, Wemmenhove鈥檚 research has made important progress in improving how mathematical proofs are taught. By creating Waterproof, they have helped students learn more effectively and made proof assistants easier to use.
This work not only enhances proof education but also helps bridge the gap between traditional methods and modern digital tools in mathematics.
Title of PhD thesis:
Supervisors: prof.dr. M.A. Peletier, dr. J.W. Portegies
