Are proof assistants the next breakthrough in mathematics? This is a question I have been thinking about since I tried the Lean proof assistant. I have tried proof assistants before, but Lean feels like it’s on another level. For one, I actually wrote a natural deduction proof in it. I can easily imagine it being usable by the average working mathematician in a few years once its user interface becomes a little more polished and installing it isn’t like installing Solaris on a microwave.
I have tried to approach this question with the parallel question of “where should mathematics go from here?” In my mind, you can’t really understand the role that proof assistants might play without also understanding the direction of mathematics. In some sense, my thoughts on proof assistants is less about proof assistants than it is about math.
Despite being a research mathematician and having spent more years than I can remember doing mathematics, I actually find it hard to articulate the exact nature of the subject. The great Bertrand Russell said that “mathematics may be defined as the subject in which we never know what we are talking about, nor whether what we are saying is true”.
I feel that the field of music, both in terms of academic study and performance, is much more clear in its purpose. Music has to sound good and be appealing and artistic to some given audience. But what of mathematics?
Mathematics is also about art, and yet there is somewhat of a strange impurity to mathematics as an art. That is, there is the problem-solving competitive aspect to it brought upon by its inherent nature of correct answers. Therefore, there is a tendency in mathematicians to push each other to constantly prove new theorems. This is ingrained in the culture, where career success is predicated on the amount of new theorems proved. Yes there is art to this evaluative procedure, but there is something besides art as well.
That tension for new results sometimes goes against the quest for beauty and understanding. This is where proof assistants can be both good and harmful. The good is rather self-evident. By having an organized system where we can store and check results, we will have a new level of understanding. Existing ideas can be clarified and new ones be more carefully formulated. We are certainly not at that level yet with existing technology, but it is possible. If we can reason it, surely so can we place that reasoning at the mercy of the machine.
But at the same time, I worry that the move towards proof assistants will also solidify the emphasis on random productivity, rather than pursuit of meaningful ideas. One argument for proof assistants is that proofs hundreds of pages long are getting hard to trust, especially since they are becoming increasingly reliant on other proofs of similar length. But how important are these proofs really? How many people actually will benefit from them, through enjoyment of an art form or otherwise, even if we knew for certain that every step was verified on a computer? And how does this look as time goes on? And more importantly, if proof assistants take over more and more details of proving something, what will the result be worth if we simply know that it is true?
I have no doubt that proof assistants will bring about an enhanced ability of humankind to prove new results in mathematics. Whether that is necessarily a good thing remains to be seen.