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