Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

May 18, 2015

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?)

Posted at May 18, 2015 8:46 PM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2824

8 Comments & 0 Trackbacks

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.

Posted by: David Jaz on May 19, 2015 3:38 AM | Permalink | Reply to this

Re: The Revolution Will Not Be Formalized

There exists a class of results jokingly known as full employment theorems – although I haven’t sketched the proof, it seems evident that a full employment theorem for mathematical proofs exists. This is to say that in some sense, there will necessarily be elements of proof search that are not automatable. Furthermore, to the extend that we understand elements of proof search enough to properly automate them, I think the world will increasingly come to view such things as “mere calculation”.

This is to say, there is no difference in kind between using a machine to multiply two very large numbers in the course of a proof and using a machine to generate and then solve a whole bunch of linear programming problems. It seems only a matter of time before people come around on the latter. (But then, of course, there will be some newer, more complicated thing, and again people will say “solving many linear programming problems, that was fine. But this, this is somehow different!”).

Posted by: Gershom B on May 19, 2015 4:05 PM | Permalink | Reply to this

Re: The Revolution Will Not Be Formalized

I share something of that point of view. One place I noticed this sort of thing myself was in developing the theory of derivators with Kate Ponto and Moritz Groth, where we frequently found ourselves needing to know that this or that square was homotopy exact. Such proofs were rarely enlightening — the important thing was finding the right squares — and seems like a good candidate for regarding as “mere calculation” by automated proof search. I even wrote a little computer program myself that could check homotopy exactness of certain types of squares between finite categories (and even produce a verified proof certificate, since it was written in Agda).

Posted by: Mike Shulman on May 19, 2015 6:46 PM | Permalink | Reply to this

Re: The Revolution Will Not Be Formalized

Nevertheless, we will never be sure

https://github.com/clarus/falso

Posted by: guest on May 19, 2015 10:20 AM | Permalink | Reply to this

Re: The Revolution Will Not Be Formalized

I remember Xavier Leroy say something like “A formalized proof allows you to offload all the boring parts of your proof from your article. So you have more time, to you know, explain it, instead of doing the boring parts”.

This really is the thing that convinced me on the future of formal proof. Not that long ago (think Lucretius’ De Rerum Natura, or Joule’s latin poems), the form was considered important in scientific writing. Nowadays, an article is disposable prose, trying in the same time to convey the ideas and to be rigorous enough. I do hope for a future where these two activities are disconnected. The article, that tries, maybe in a poetic and slightly incorrect way, to transmit pure thought. And, alongside of it, the mechanized proof, that contains all the tedious details.

Posted by: Luc Pellissier on May 20, 2015 1:06 PM | Permalink | Reply to this

Re: The Revolution Will Not Be Formalized

Reading through the actual book Mathematics without apologies (or, to be honest, skimming through it), I came across the following quotation, which I think epitomizes the confusion among many people about computer verification of proofs:

…in its advice to prospective authors of mathematical articles, the American Mathematical Society (AMS) gives tricks a positive valuation: “Omit any computation which is routine (i.e., does not depend on unexpected tricks). Merely indicate the starting point, describe the procedure, and state the outcome.”…

Voevodsky’s vision of mathematical publication cleared by automated proof checkers, if realized, will require the AMS to countermand current policy. All routine computations will have to be included in order to satisfy the expert system gatekeeper who guards the border with no orders to distinguish tricks from the routine. Ambivalence to tricks, even the sense that tricks form a separate genre, will then be seen as yet anotnher transitory feature of the mathematics of the human period.

As I’ve said above, almost none of this is true (though a mathematician who is unfamiliar with how computer verification actually works can certainly be forgiven for thinking it).

It is true that routine computations must be verified along with tricks. However, that’s only true of the computer-formalized proof; the version of the proof written for humans can still omit them. This is true even if, as is done with dialects such as “literate Agda”, the two versions of the proof are produced from the same “source code” (a hybrid of TeX and Agda) — in this case, separate “compilation” commands strip out the fluff for the computer reader and strip out the uninteresting computations for the human reader.

Moreover, as mentioned in several comments above, the “routine computations” are exactly those bits of the proof most susceptible to true automation (rather than mere verification). Thus, one may hope that eventually the author of a paper will not need to take the time to write them out either. (Indeed, one may argue that robust automation of this sort is one of the preconditions for widespread adoption of computer verifiers — mathematicians don’t want to have to write out those computations themselves either!) Thus, eventually the situation will be no different from the current AMS guidelines; the only difference will be that the computer will do the computations for us in the background, so that we don’t have to worry about whether or not they are correct.

Posted by: Mike Shulman on May 26, 2015 7:39 PM | Permalink | Reply to this

Re: The Revolution Will Not Be Formalized

I would add that routine computations, by Murphy’s Law (one of the most important laws in all fields), are probably most likely to be wrong. Which, I suppose, is not too much of a problem with regards to proofs, as long as they are only wrong in routine ways.

We should not underestimate encoding just “runnable” elements of proofs in computers, even if we do not entirely verify them. For one, some systematic randomized testing can inspire a higher degree of confidence even without full formalization. And furthermore, automated probing can track down results of interest that can then be further analyzed by humans.

A nice example of this is provided in this nice review by Simon Thompson of a recent study on “regular algebra”.

Posted by: Gershom B on May 29, 2015 5:44 AM | Permalink | Reply to this

Re: The Revolution Will Not Be Formalized

I would add that routine computations, by Murphy’s Law (one of the most important laws in all fields), are probably most likely to be wrong. Which, I suppose, is not too much of a problem with regards to proofs, as long as they are only wrong in routine ways.

Thanks for this! I started to write the following response:

“I guess if you mean that when someone writes out a routine computation they are likely to make a mistake, then yes, I agree. But I think the point is more that routine computations often aren’t written out in published papers at all, and I would expect that their routine-ness means that the correctness of the result is not in doubt; if you try to verify it and it doesn’t work out, it probably just means that, as you say, you made a routine mistake in your verification.”

But then I remembered that in subjects other than category theory, people sometimes perform computations for which they don’t know the result in advance! (-:O And in such a case, it might be the case that the author of the paper made a routine mistake in the computation, and that in turn might lead to incorrect proofs even of conceptual results (e.g. by believing that an obstruction vanishes when it does not).

On the other hand, unverified computer computations can also make “routine mistakes” (a.k.a. “bugs”).

Posted by: Mike Shulman on May 29, 2015 5:31 PM | Permalink | Reply to this

Post a New Comment