[FOM] Proof assistants and conjectures
Roger Bishop Jones
rbj at rbjones.com
Wed Jan 7 03:44:24 EST 2009
On Monday 05 January 2009 04:37:39 Timothy Y. Chow wrote:
> For the most popular proof assistants, has there has been any systematic
> effort to compile databases of conjectures as well as of theorems?
There is a list of "The Hundred greatest theorems" at:
http://personal.stevens.edu/~nkahl/Top100Theorems.html
There is a page devoted to tracking formal proofs of these theorems at:
http://www.cs.ru.nl/~freek/100/index.html
This tracks progress in proving the "100 theorems" by eight proof assistants.
These are typically formal proofs concocted by people using software which
aids and abets construction of the proof and ensures its correctness..
I don't think any two of the 8 participant provers accept the same notation,
and this is the principle difficulty with the provision of a standardised
list of theorems. Four of the proof tools have an online list of the
theorems so you can compare the notations.(and sometimes see the proofs or
proof scripts).
The situation is exacerbated by the fact that most things proven by such proof
assistants depend for their statement and proof on extensive libraries of
prior definitions and theorems. Even if the notation were translated (which
often will be straightforward) the lack of uniformity in the libraries would
be an impediment to standardisation of the statement of the theorems.
This is still an advancing research effort which is well short of where we
would like it to be, so there is no prospect at present of stabilisation.
The situation is different in automatic theorem provers, particularly for
first order logic, where such lists are available.
Roger Jones
More information about the FOM
mailing list