Jim Portegies has just started a remarkable project with a couple of students in Analysis 1. His long-term aim is to develop a language and a computer-based setup that will help students to learn to construct proofs.

The idea is a combination of some independent developments. The first is that so-called proof assistants are quickly becoming more powerful, with large prebuilt libraries currently available, and many possibilities for extending the language. Such systems assist the human mathematician by continuously checking arguments for rigour while providing search algorithms for exploring the space of rigorously provable facts. However, these systems currently have a steep learning curve, and in current form they would not be useful as tools for learning. The second development is our own experience at the TU/e with automatic exercise-checking for courses like calculus, where students can submit their exercises an unlimited number of times for checking; many students indeed do this, and the instant feedback on their mistakes provides for very efficient learning. Jim’s experiment is all about developing proof assistants into tools that students can use to learn what a proof really is and how one invents new proofs.

The long-term view is to have a system that closely mirrors how we mathematicians think about proofs, but in the meantime Jim and a number of students of Software Engineering have already started building a first version, called Waterproof, which also is freely available on github. This is what a lemma looks like in the Waterproof language:

Lemma auxiliary_lemma :
  for all x z : ℝ,
    (for all ε : ℝ, ε > 0 ⇒ x > z - ε) ⇒
      x ≥ z.

It says that for any two real numbers x and z, if x is larger than z - ε for any positive ε, then x is larger or equal than z. Once one gets used to the notation this statement is fairly easy to read.

And this is what its proof looks like:

Proof. 
Take x : ℝ. Take z : ℝ. Assume H1 : 
  (for all ε : ℝ, ε > 0 ⇒ x > z - ε).
  
We claim that (¬ (x < z)) (not_x_lt_z).
  We need to show that (x < z ⇒ False).
  Assume x_lt_z : (x < z).
  It holds that (0 < z - x) (H2). 
  It holds that (x > z - (z - x)) (H3). 
  Write H3 using (z - (z-x) = x) as (x > x).
  It holds that (¬ (x > x)) (H5).
  Contradiction.
It follows that (x ≥ z).
Qed.

What I find remarkable is that also this code for the proof is so readable for a human being. Yes, it is more complicated than what we would normally write ourselves, and it contains many steps that we would skip, but keep in mind that this proof can be read and checked by a computer.

At this moment a number of students have signed up as beta-testers, and they are currently doing some of their Analysis 1 exercises in this computer-based environment. I’m looking forward to hear their experiences, and how this computer-assisted-learning-to-prove system evolves . . .