Waterproof - Transforming a Proof Assistant into an Educational Tool
Institut Henri Poincaré via YouTube
Overview
Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Learn how to transform a proof assistant into an effective educational tool through this conference talk that explores the development of Waterproof, an innovative software designed to help students master mathematical proof-writing skills. Discover how researchers at Eindhoven University of Technology created this educational platform, which combines a Rocq plugin with a Visual Studio Code extension to bridge the gap between formal proof assistants and traditional paper-based proof writing. Examine the design philosophy behind using controlled natural language to make digital proof construction feel as intuitive as writing proofs by hand. Explore the various design decisions that shaped Waterproof's development, including user interface considerations and pedagogical approaches that prioritize student learning outcomes. Review evaluation methodologies and results that demonstrate the software's effectiveness in educational settings, including student performance metrics and usability studies. Investigate preliminary research into integrating large language models as intelligent tutoring systems that can provide personalized guidance and hints to students working through mathematical exercises. Gain insights into the challenges and opportunities of modernizing mathematical education through technology while maintaining the rigor and clarity essential to proof-based learning.
Syllabus
Waterproof: transforming a proof assistant into an educational tool
Taught by
Institut Henri Poincaré