According to many mathematicians a major shift is taking place in the mathematics research landscape. Mathematicians and big tech companies are working intensively to formalize (i.e. translate to a format that can be read by a computer) mathematical proofs and verify their correctness using so-called proof assistants. Long research articles, which typically take months to review, could be verified in a day by using such new tools. This opens new paths in mathematics research.
Such major shifts often also have an effect on education. For example, to support students to acquire the skill of writing 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, thanks to the work of Jim Portegies, they have embodied this technology in Waterproof, which is used since 2019 in the undergraduate program in mathematics. Waterproof's use of controlled natural language allows students to write proofs as they would with pen and paper, and reduces the steep learning curve of traditional proof assistants.
Seeing the momentum in this direction, AMI decided to finance the Strategic Education Initiative 'Waterproof: Proof assistants for mathematics education'. This SEI aims to expand Waterproof to other mathematics programs within our partner institutes. Moreover, Jim recently received an NRO Scale-up grant which will support this endeavor to run pilots with Waterproof in other programs and universities. We thought this is a perfect moment for an interview with Jim, to hear from him how this project started and which are his goals for the future.
First of all, Jim congratulations with your recent NRO Scale-up and AMI grants! Can you tell us how this project with Waterproof started?
We started with this idea in 2018 when a bachelor student did a project on proof assistants and how such a tool could be included in our first year course on Analysis. In 2019 a group of eleven computer science students worked on developing a first version of the software as part of a software engineering project. Typically, writing a proof in a proof assistant isn’t always the same as how we teach students to write formal proofs and can be cumbersome to understand. Our main goal was to make the program more friendly for students, compared to other proof assistants. It was important for us that they could write proofs in Waterproof as they do with pen and paper. Moreover, their proofs should be readable without having to dive into the syntax of the proof assistant. When the program was ready, we ran a pilot with a group of students which looked very promising.
In this Analysis course students typically work in groups of four. When we started with the pilot, some solutions could be submitted in Waterproof, next to the assignments that should be submitted on paper. But, after a few years, when we had gained enough experience, we decided that each student should submit an individual solution in Waterproof. This individual assignment seems to have been beneficial for the learning of many students. With a group submission we saw that usually a couple of students would take the lead and make the assignments. These students would also become very skilled at the course. But this wasn’t the case for the rest of the students. With individual assignments in Waterproof, everybody practices and it seems that more students develop the intended skills.
Can you give us some insights from your experience about how students benefit from Waterproof?
We have observed that the students who have difficulties with the first steps in how to write a proof can profit significantly from Waterproof. When we introduced the individual assignment we observed that these students started improving and getting higher grades. In an analysis course many steps are mechanical. They are not so difficult to understand conceptually, but they need repetition to master. The advantage of writing a proof in Waterproof is that students can practice with such mechanical steps and check if their proof is correct before submitting it. They get feedback by the program and they can work on it until it is correct.
Personally, I think it is very important for students to learn at an early stage to write neat and compact proofs. They should develop a good intuition on how they should write specific arguments in a neat and compact manner. Moreover, they should develop a toolkit of arguments they can automatically write down when they use specific techniques. Waterproof can support this process because of the restrictions it imposes on how you can write your arguments. You can’t just write anything you want.
Furthermore, in a course like analysis, we have 300 students and it is not possible to give good feedback to all of them in a classical way. Tools like Waterproof can support both teachers and students in such large courses. But it is important to realize that adding such a tool in a course should have a clear goal and it should be properly aligned with the other learning activities. We keep experimenting with Waterproof and evaluate what works well.
This year we also developed Waterproof River where we have included feedback from an LLM which can spot syntax mistakes very efficiently. Teachers can then focus on more challenging and interesting aspects of the course. For students it is important to explore what helps them during their learning process. For example, some LLM’s, if used properly, can give very good feedback on mathematical proofs. There is a tool called HaLLMos which can give surprisingly good feedback in natural language on a written proof.
Can you give us a trailer of your future plans?
I strongly believe that working with proof assistants will become an essential skill for mathematicians. 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. 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.
With the NRO and AMI educational grants we can scale up using Waterproof to other mathematics programs. We will collaborate with mathematicians from Groningen and the VU who will include Waterproof to their analysis courses, similar to what we do in Eindhoven. We will also run pilots in a first year course on formal mathematical proofs in Utrecht and Delft. With these grants we also aim to form a clear idea how new teachers can make a start with Waterproof and include it in their courses. The long term goal is to make it as easy as possible to add Waterproof in a course and eventually support more students to learn how to write mathematical proofs.
