Partial answers to some old questions about proof assistants
Timothy Y. Chow
tchow at math.princeton.edu
Tue Feb 23 09:48:41 EST 2021
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
More information about the FOM
mailing list