3 papers
math.HO2026
The Educational Proof Assistant Waterproof in an Introductory Proof Course: Proof Construction and Learning Processes
Pim Otte, Rogier Bos, Johan Commelin +1
We study the use of an educational proof assistant in an introductory proof course through a quasi-experiment in a varied setting: multiple teachers, students with different study…
math.HO2026
Waterproof Editor: an educational environment for proof assistants and programming languages
Pim Otte, Dick Arends, Raul Sánchez Flores +2
Waterproof Editor provides an educational environment specifically targeted to teaching with proof assistants or programming languages. It arose from Waterproof, educational softwa…
cs.LO2025
Tutte's theorem as an educational formalization project
Pim Otte
In this work, we present two results: The first result is the formalization of Tutte's theorem in Lean, a key theorem concerning matchings in graph theory. As this formalization is…