Waterproof: Educational Software for Learning How to Write Mathematical Proofs
Jelle Wemmenhove, Dick Arends, Thijs Beurskens, Maitreyee Bhaid, Sean, McCarren, Jan Moraal, Diego Rivera Garrido, David Tuin, Malcolm Vassallo,, Pieter Wils, Jim Portegies

TL;DR
Waterproof is an educational tool based on Coq that helps students learn to write mathematical proofs by providing feedback and a specialized interface, improving understanding and clarity.
Contribution
The paper introduces Waterproof, a tailored proof assistant with a custom language and editor designed specifically for teaching proof writing in mathematics courses.
Findings
Students improved their understanding of proof structure.
Explicit proof language clarified logical reasoning.
Tool successfully integrated into university coursework.
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. Like with other interactive theorem provers, students write out their proofs inside the software using a specific syntax, and the software provides feedback on the logical validity of each step. Waterproof consists of two components: a custom proof language that allows formal, machine-verified proofs to be written in a style that closely resembles handwritten proofs, and a custom editor that allows these proofs to be combined with formatted text to improve readability. The editor can be used for Coq documents in general, but also offers special features designed for use in education. Student input, for example, can be limited to specific parts of the document to prevent exercises from being accidentally deleted. Waterproof has been used to…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMathematics, Computing, and Information Processing · Logic, programming, and type systems · Mathematics Education and Teaching Techniques
