Some thoughts on proof assistants

A proof assistant is a computer program that takes as input a proof in a formal language and outputs true if and only if the proof is a valid proof in a formal system. An example would be first-order logic with its inference rules.

Proof assistants are supposed to tell you whether your proof is correct. Every once in a while, I test one out for fun. Recently I noticed Lean, a proof assistant or theorem prover from Microsoft that I'd like to try. In the context of proof assistants, I think the ideal for most mathematicians would be to actually have an intuitive system where you could easily write proofs for the system and have your proof verified in seconds. We are definitely far from that goal. But proof assistants nevertheless pose some interesting questions: what is wrong with verifying proofs by hand, and what do proof assistants imply for the future of mathematics?

I was struck by a the talk Univalent Foundations of Mathematics by Vladiimir Voevodsky, in which he talks a little about proof assistants. He also talks about an alternative foundation of mathematics based on types, and the two are intertwined because at the time he was interested in using a proof assistant based on types. Ostensibly Voevodsky seemed interest in this avenue with regard to a possible inconsistency in pure math, but from his talk, it seems that he was at least equally concerned with his increasingly complex proofs in the area of motivic cohomology. More specifically, his concern was that very few people would read these proofs, verify and believe them.

That at least partially tells us why verifying proofs by hand may not always work. I also read an article somewhere where another mathematician suggested that math is becoming so complex that we will eventually need proof assistants in order to keep the machine going. In one regard, I actually think proof assistants in their ideal incarnation would be great for math. It might actually help the incredibly long wait times for referee reports. Proof assistants would also help us write papers more quickly, akin to how a compiler allows us to write code more quickly if we frequently recompile. That's assuming writing proofs in a proof assistant would be nearly as easy as writing them out in our usual informal style.

I do think there is something to fear regarding proof assistants, and it has nothing to do with the possibility of computers one day proving stuff better than humans. Rather, I fear that mathematics is going down the road of increasing complexity for the sake of keeping our traditional machine of mathematics running, and that proof assistants will only validate and keep that going. By this I mean people writing highly technical papers for the sake of writing a paper. At some point, we might have to ask ourselves if the traditional model of publishing hundreds of random papers a day is actually good for anything, but that point might never come if we happen to be too clever and invent proof assistants so powerful that they can deal with any level of complex mathematics.

To be clear, I think pure mathematics for the sake of mathematics is great, and I don't think it should ever stop. However, that can only really work if people are doing mathematics for the sake of its artistic value. If we instead have an environment that encourages random publications then it will become a cultural norm and trend to continue with ever increasing microcosms that generate these publications. These random publications often have little intrinsic interest and thus their value is essentially a system that validates a person's ability to do and teach math. Proof assistants, while really interesting and cool, also have the potential to be a disruptive technology to facilitate such a culture to new extremes, and that is something to which we should give serious thought.

Leave a comment

Fields marked with * are required. LaTeX snippets may be entered by surrounding them with single dollar signs. Use double dollar signs for display equations.