Partial answers to some old questions about proof assistants

[Timothy Y. Chow]

In the past, I have posed some questions here on FOM about proof 
assistants.  With the passage of time, answers (or at least partial 
answers) have emerged to some of those questions.  I want to make some 
brief comments here about these, mostly for my own benefit, but also for 
the benefit for any other FOM readers who were interested in the same 
questions.

1. In 2009, I asked whether there has been any systematic effort to 
compile databases of *conjectures*.

https://cs.nyu.edu/pipermail/fom/2009-January/013262.html

Nowadays, the closest thing seems to be the Formal Abstracts project, 
which I believe was started by Tom Hales in 2017.

https://formalabstracts.github.io/

The vision of the Formal Abstracts project isn't quite the same as what I 
had in mind; the idea is to write down formal versions of statements of 
*theorems*, but the point is that there is no need to write down the 
entire proof.  So the same methodology could presumably be used to 
assemble a list of formally stated conjectures.

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

Tim Chow