Waterproof: Proof assistants for mathematics education
Abstract/description
To help students with acquiring the skill of mathematical proofs, more and more teachers are turning to proof assistants. These tools provide immediate feedback on mathematical proofs, and in the end verify their correctness. In Eindhoven, we have embodied this technology in Waterproof, educational software that helps students write mathematical proofs. Waterproof's use of controlled natural language helps students transfer the skills they acquire to writing proofs on paper and reduces the steep learning curve of traditional proof assistants.
These developments occur in a broader context where proof assistants, especially in conjunction with generative AI, are becoming increasingly important in mathematics and are changing the mathematical landscape itself. The large academic interest is complemented by unprecedented commercial interest, with companies such as Harmonic, Google Deepmind, Morph Labs, OpenAI, Math Inc, investing enormous amounts of resources into teaching computers to do mathematics. An important reason why is that proof assistants provide a unique tool: they can actually verify AI-generated output, weeding out hallucinations and providing a trustworthy feedback signal that can be leveraged in reinforcement learning. Given these advantages, proof assistants are expected to play an increasingly large role in Mathematics, Computer Science, and related fields. Waterproof also helps prepare students and teachers for these developments.
Both because we see the benefits for education, and because we believe that proof assistants in combination with generative AI will play a large role in education and research, we see it as crucial to embed the necessary expertise into the 4TU+.AMI community. We would like to build a community within 4TU+.AMI around proof assistants for education and make teaching with proof assistants practically feasible. By facilitating teaching with Waterproof, we will also be able to observe how Waterproof performs in different educational contexts and further improve it. We envision that this involvement will speed up the adoption of formal proofs and proven algorithms to the broader 4TU+.AMI community and enable a more effective use of new tools such as AlphaProof and AlphaEvolve, in mathematics.
This SEI started on 01-11-2025 and aims to reach its goals before 01-11-2026.
Goals
General scope: In this project we will support pilots with Waterproof in Groningen, in the Analysis course taught by Marcello Seri, and at TUD in the Problem-solving and Proofs course taught by Bart van den Dries. We will focus on developing exercises, creating documentation both in written and video form, and on further developing the software.
Software development: whereas our software development so far has been focused on the students, in this project we will also aim to make the software more convenient to use from the teacher's perspective, especially when it comes to designing exercise sheets.
Recently we have had very successful experiments for using generative AI for writing proofs in the Waterproof proof language. A current internship now explores various possibilities for giving extra support to students within Waterproof. In the context of this proposal, we will implement the resulting design from the internship into the actual software.
Waterproof hackathons: we will organize four Waterproof hackathons. These hackathons will allow teachers to get hands-on experience with the tool, and suggest and in some cases even implement improvements. In Groningen and Delft, the sessions will prepare teachers for the pilots that involve teaching with Waterproof.
At the end of the project, we will organize a joint evaluation afternoon, with several interactive sessions in which people can share their experiences and provide further feedback to direct future development of the project.
Contact person
- Jim Portegies (TU/e)
Participants
- Marcelo Seri (RUG)
- Bart van den Dries (TU Delft)
- Tamás Görbe (RUG)
- Alexander Schüler-Meyer (TU/e)