Waterproof: educational software for learning how to write mathematical proofs

Research output: Contribution to journalArticleAcademic

113 Downloads (Pure)


In order to help students learn how to write mathematical proofs, we developed the educational software called Waterproof (https://github.com/impermeable/waterproof). Waterproof is based on the Coq proof assistant. As students type out their proofs in the program, it checks the logical soundness of each proof step and provides additional guiding feedback. Contrary to Coq proofs, proofs written in Waterproof are similar in style to handwritten ones: proof steps are denoted using controlled natural language, the structure of proofs is made explicit by enforced signposting, and chains of inequalities can be used to prove larger estimates. To achieve this, we developed the Coq library coq-waterproof. The library extends Coq's default tactics using the Ltac2 tactic language. We include many code snippets in this article to increase the number of available Ltac2 examples. Waterproof has been used to supplement teaching the course Analysis 1 at the TU/e for a couple of 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.
Original languageEnglish
Article number2211.13513
Number of pages28
Publication statusPublished - 24 Nov 2022

Bibliographical note

The Waterproof software can be found at https://github.com/impermeable/waterproof . This article pertains to Waterproof version 0.6.1. The Coq library coq-waterproof can be found at https://github.com/impermeable/coq-waterproof . This article pertains to coq-waterproof version 1.2.4


Dive into the research topics of 'Waterproof: educational software for learning how to write mathematical proofs'. Together they form a unique fingerprint.

Cite this