Partial answers to some old questions about proof assistants

[Lawrence Paulson]

The belief you refer to may have come from the type theory world and probably refers to the idea that computer verification of a proof can deliver a certificate that can be checked, independently of the original verification software. This is true of many current systems, but there is no reason to believe that the certificate will be concise and capable of being checked quickly: though at least it could be checked more quickly than repeating the computer verification from scratch.

As there is no agreed format for such certificates, this approach cannot work when (as in the case of Flyspeck) different interactive theorem provers were used for different parts of the proof.

In fact these certificates turn out to be extremely large, which is why some of us prefer to do without them altogether.

Larry Paulson



> On 23 Feb 2021, at 14:48, Timothy Y. Chow <tchow at math.princeton.edu> wrote:
> 
> 2. In 2007, and a couple of times since then, I have questioned a belief that seemed to me to be widespread, that computer verification of any single proof would be an almost instantaneous computation on a single processor, and would confirm its correctness all the way down to the axioms. But it seemed to me that there are increasingly many proofs that are far too complicated for this, and that maintaining a database of them would involve highly nontrivial knowledge management problems.
> 
> https://cs.nyu.edu/pipermail/fom/2007-June/011667.html
> https://cs.nyu.edu/pipermail/fom/2014-August/018057.html
> https://cs.nyu.edu/pipermail/fom/2016-January/019452.html
> 
> I recently learned of a very interesting talk by Mark Adams called "Flyspecking Flyspeck" which confirms that these knowledge management problems are real, and goes into some detail about them in the case of Flyspeck.
> 
> https://mathematics.pitt.edu/hales60/pdf/Adams-Mark.pdf