What work has been done on computationally intensive proofs?

Question

Fifty years ago, few would have imagined that the process of verifying the correctness of a known proof of a mathematical theorem might be so costly that the mathematical community would hesitate to do it more than once. Of course, nowadays, there is a growing list of theorems whose proofs require an enormous amount of computation. In many cases, these theorems amount to calculating the first few values of an infinite sequence of values, and maybe not many people would care to have those computations formally verified. In other cases, however, there is an attractive theorem statement that many might want to see a formal proof of. The Kepler conjecture is an obvious example; perhaps less well known to the proof-assistant community is the ternary Goldbach problem, solved by Harald Helfgott, who reduced the problem to a feasible finite computation. A complete proof therefore requires doing this computation; to give some idea of how big this computation is, let me quote a paragraph from Helfgott's preprint:

In December 2013, I reduced $C$ to $10^{27}$. The verification of the ternary Goldbach conjecture up to $n \le 10^{27}$ can be done on a home computer over a weekend, as of the time of writing (2014). It must be said that this uses the verification of the binary Goldbach conjecture for $n \le 4 \cdot 10^{18}$ [OeSHP14], which itself required computational resources far outside the home-computing range. Checking the conjecture up to $n \le 10^{27}$ was not even the main computational task that needed to be accomplished to establish the Main Theorem—that task was the finite verification of zeros of $L$-functions in [Plab], a general-purpose computation that should be useful elsewhere.

Proofs like these seem to pose a significant knowledge management problem if we envisage a future in which the majority of interesting mathematical results are archived in some machine-checkable library. It seems that if we want to check the proof of a new theorem that relies on an existing theorem whose proof is extremely expensive, then we are faced with the choice of either redoing the expensive computation, or taking it on faith that someone else checked it and that we haven't made a bookkeeping error somewhere along the way. If there are only a few expensive theorems then maybe there isn't a problem, but if expensive theorems proliferate, and we want to rely on our records of whether they were checked or not, then it seems that the chances of mistakenly thinking that something was proved (when it really wasn't) start to become non-negligible. This is especially true if we have software "upgrades" every couple of years that could introduce bugs, or at least confusion over the exact meanings of various terms and theorems.

With the above remarks as background, I have a twofold question.

1. Do existing systems have a plan for managing this kind of issue? I see that there is another question about recompilation avoidance that seems related, but doesn't seem to be quite the same.

2. Typically, how much computational overhead is there when we take a conventional computation and redo it in a proof assistant? (Here, I'm not talking about the human effort in doing the re-programming, although I recognize that that is also a major issue.) The answer is probably, "It depends," but I'm wondering if there is any rule of thumb. In this regard, I found the Ph.D. thesis of Muhammad Taimoor Khan, Formal Specification and Verification of Computer Algebra Software, to be very interesting. For certain types of computation in Maple, one can apparently answer this question fairly easily by running Khan's software. Are there other packages available that allow someone with conventional programming experience but little experience with proof assistants to write "normal-looking code" (or something close to it) that carries out a formally verified long computation, and thereby time how much longer it takes than conventional code does?

Answer 1

You are touching upon some questions that we are currently investigating in our research group, but we do not have definite answers yet, so let me just make a couple of comments regarding the trade-offs.

Consider a computationally expensive verification of some mathematical fact, e.g. something that requires lots of large number arithmetic, symbolic computation, Gröbner basis computations, SAT solving, etc. In all such cases there we use specialized algorithms that are implemented using traditional software tools and made to run fast. How could we incorporate them into a proof assistant? There are several options, depending on how we trade speed for trust:

1. We can incorporate external libraries into a proof assistant and trust them. Many proof assistants trust that number arithmetic is correctly implemented, say in the GMP library. Trusting Mathematica sounds insane, but incorporating Mathematica into Lean is worthwhile, and one can do things to increase the trust.

2. We can incorporate external libraries into a proof assistant and formally verify them to be correct. This would be the ideal solution, but I am not aware of any such efforts. It sounds difficult to do.

3. We can reimplement algorithms inside a proof assistant, together with proofs that they perform correctly. These can then be extracted to efficient code or compiled to native code on the fly. Of course, one then has to trust a larger chunk of the proof assistant.

The third solution will always lag behind the first one, and so one will always be tempted to trade trust for speed. But is this such a bad idea? I would argue that we should allow use of non-trusted software components, but also devise methods that track the provenance, so that we can tell which result depends on correctness of what software.

Answer 2

Not as general as Andrej's answer but more a data-point for your interest. We've been looking at how to construct formal proofs about neural network-enhanced systems in proof assistants. This runs into exactly the problem you describe: the act of verifying the network can be very expensive (hours/days) which disrupts the interactive component of the proof assistant.

As described in Figure 1 in our recent paper, we've taken the external book-keeping approach, i.e. create a cache which stores the result of the verification of the network. The proof assistant then checks the cache instead of reverifying the network each time. The cache maintains consistency by also storing the location and the hash of the network, which can be used to detect when the proof has become invalid (for example due to further training of the network).