Waterproof: Demo of an educational tool built on a theorem prover

Pim Otte


Date: Wed, June 18, 2025
Time: 12:00
Room: building 28, Turing


The key skill for a mathematician is being able to write down proofs of theorems. Waterproof is an educational software tool that aims to teach this skill to mathematics students, built on top of the Rocq theorem prover. The goal of this tool is to provide students with an environment that gives immediate feedback, while resulting in a proof that would also be accepted on paper. In this talk I will demonstrate the Waterproof tool, discuss the benefits and challenges of building on top of the Rocq theorem prover, discuss the practical learnings from applying this in teaching at the Technical University of Eindhoven and (if time permits) dive into the details of recent improvements inspired by these learnings.

Previous: Maria Khakimova |
Next: