The n-Category Café

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.

Nevertheless, we will never be sure

https://github.com/clarus/falso

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.

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.