Waterproof: educational software for learning how to write mathematical proofs

Jelle Wemmenhove, Thijs Beurkens, Sean McCarren, Jan Moraal, David Tuin,
and Jim Portegies, Eindhoven University of Technology (TU/e), Eindhoven, The Netherlands

Abstract

In order to help students learn how to write mathematical proofs, we adapt the Coq proof assistant into an educational tool we call Waterproof 1. Students interact with the software the same way as they would with other interactive theorem provers: they type out their proof step-by-step and they can request the program to check the validity of each step and provide feedback. Unlike with Coq, the proofs written in Waterproof are similar in style to regular mathematical proofs. This is achieved with the custom Coq library coq-waterproof. The second component to Waterproof is a custom editor that is designed with an educational setting in mind. For example, certain parts of a file can be locked such that they are not accidentally deleted by students. Waterproof has been used to supplement teaching the Analysis 1 course at Eindhoven University of Technology (TU/e) for the last four years. Students started using Waterproof’s controlled formulations of proof steps in their handwritten proofs as well; the explicit phrasing of these sentences helps to clarify the logical structure of their arguments.