### The Revolution Will Not Be Formalized

#### Posted by Mike Shulman

After a discussion with Michael Harris over at the blog about his book Mathematics without apologies, I realized that there is a lot of confusion surrounding the relationship between homotopy type theory and computer formalization — and that moreover, this confusion may be causing people to react negatively to one or the other due to incorrect associations. There are good reasons to be confused, because the relationship is complicated, and various statements by prominent members of both communities about a “revolution” haven’t helped matters. This post and its sequel(s) are my attempt to clear things up.

In this post I will talk mainly about computer formalization of mathematics, independently of homotopy type theory. There are multiple applications of computers to mathematics, and people sometimes confuse computer *verification* of proofs with computerized *automated proof-finding*. Homotopy type theory has very little to do with the latter, so henceforth by “formalization” I will mean only the *verification* of proofs.

This often means the verification of *pre-existing* proofs, but it is also possible to use a computer to help construct a proof and verify it at the same time. The tools that we use to verify proofs incorporate a small amount of automation, so that this process can sometimes save a small amount of effort over writing a proof by hand first; but at least in the realm of pure mathematics, the automation mainly serves to save us from worrying about details that the computer cares about but that we wouldn’t have worried about in a paper proof anyway.

Computer-verified proof has been going on for decades. Recently it’s garnered a bit more attention, due partly to complete verifications of some “big-name” theorems such as the four-color theorem, the odd-order theorem, and the Kepler conjecture, whose proofs were so long or complicated or automated that reasonable mathematicians might wonder whether there was an error somewhere.

What is the future of computer-verified proof? Is it the future of mathematics? Should we be happy or worried about that prospect? Does it mean that computers will take over mathematics and leave no room for the humans? My personal opinion is that (1) computer-verified proof is only going to get more common and important, but (2) it will be a *long time* before all mathematics is computer-verified, if indeed that ever happens, and (3) if and when it does happen, it won’t be anything to worry about.

The reason I believe (2) is that my personal experience with computer proof assistants leads me to the conclusion that they are still very far from usable by the average mathematician on a daily basis. Despite all the fancy tools that exist now, verifying a proof with a computer is usually still a *lot* more work than writing that proof on paper. And that’s *after* you spend the necessary time and effort learning to use the proof assistant tool, which generally comes with quite a passel of idiosyncracies.

Moreover, in most cases the benefits to verifying a proof with a computer are doubtful. For big theorems that are very long or complicated or automated, so that their authors have a hard time convincing other mathematicians of their correctness by hand, there’s a clear win. (That’s one of the reasons I believe (1), because I believe that proofs of this sort are also going to get more common.) Moreover, a certain kind of mathematician finds proof verification fun and rewarding for its own sake. But for the everyday proof by your average mathematician, which can be read and understood by any other average mathematician, the benefit from sweating long hours to convince a computer of its truth is just not there (yet). That’s why, despite periodic messianic claims from various quarters, you don’t see mathematicians jumping on any bandwagon of proof verification.

Now there *would* be certain benefits to the mathematical community if all proofs were computer verified. Notably, of course, we could be sure that they were correct. If all submissions to journals were verified first by their authors, then referees could be mostly absolved of checking the correctness of the results and could focus on exposition and interest. (There are still certain things to check, however, such as that the computer formalization does in fact prove what the paper claims that it does.)

I can imagine that once there is a “critical mass” of mathematicians *choosing* to verify their own results with a computer, journals might start requiring such verification, thereby tipping the balance completely towards all mathematics being verified, in the same way that many journals now require submissions in (La)TeX. However, we’re a long way from that critical mass, because proof assistants have a long way to go before they are as easy to use as TeX. My guess is that it will take about 100 years, if it happens at all. Moreover, it won’t be a “revolution” in the sense of a sudden overthrow of the status quo. Historians might look back on it afterwards and call it a revolution, but at the time when it happens it will feel like a natural and gradual process.

As for (3), for the most part computer verification is just a *supplement* to ordinary mathematical reasoning. It’s a tool used by human mathematicians. We have to learn to use it correctly, and establish certain conventions, such as the fact that you’ve verified a proof with a computer doesn’t absolve you from explaining it clearly to humans. But I have faith that the mathematical community will be up to that task, and I don’t see any point in worrying right now about things that are so far in the future we can barely imagine them. (And no, I don’t believe in the AI singularity either.)

(Next time: What about HoTT?)

## Re: The Revolution Will Not Be Formalized

This is not entirely on-topic, but something I have been thinking about recently.

Some of the comments floating around the web about automated proof-finding, as you’ve called it, remind me of my granddad’s quip to my dad when he started working with computers: “Be careful, or you’ll end up eating the chips.” The idea seems to be that mathematicians will write ourselves out of mathematics with automated proving. I think this undersells the kind of conceptual changes we would have to undergo to be able to automate ‘proving’ in some way like mathematicians actually do it. It shouldn’t just mean more clever algorithms, but new ways of understanding the search space of proofs, new ways of conceiving of mathematical contexts and definitions and the way they change and interact ‘prior’ to their formalization. I have no idea if this view is shared by actual researchers in the field, but it seems that the creation of automated proving systems is a criterion for success in coming to a formal understanding of the process of making mathematics, rather than the goal.

For me, the aims of automated proving research are divided between the grand and the gritty. The gritty could be called ‘automated lemma proving’, where the goal is to make proof systems that can prove lemmas or small theorems specified by users. These systems, especially ones that use heuristics and can TeX up descriptions of their ‘reasoning’, could be very useful for finding the ‘right’ formal system for a scientific or mathematical problem. They could let a researcher have a hunch about a structure, and then work with a machine to create an ‘elementary theory’ of that structure. This might make it easier to find natural homes for problems that might not have been found in the usual pastures.

The grand aim would be to tell a formal story about the process of making mathematics, the development of ideas into proofs and theories. Maybe this is a pipe dream of mine, but I think there are good stories to tell about mathematical context, meaning, and definition. And since stories about mathematics can often be retold mathematically, I think there’s something going on here that will not be exhausted by the theory needed to make a successful lemma prover. However, if we were to tell mathematical stories about the process of making math, automated proof systems could demonstrate that those stories pull their weight.